Theorem mdsymlem3 10327

Description: Lemma for mdsym 10333.

Hypotheses

Ref	Expression
mdsymlem1.1	|- A e. CH
mdsymlem1.2	|- B e. CH
mdsymlem1.3	|- C = (A vH p)

Assertion

Ref	Expression
mdsymlem3	|- ((((p e. Atoms /\ -. (B i^i C) (_ A) /\ p (_ (A vH B)) /\ A =/= 0H) -> E.r e. Atoms E.q e. Atoms (p (_ (q vH r) /\ (q (_ A /\ r (_ B)))

Distinct variable groups:   r,q,C   q,p,r,A   B,p,q,r

Proof of Theorem mdsymlem3

Step	Hyp	Ref	Expression
1		atelch 10266	. . . . 5 |- (p e. Atoms -> p e. CH)
2		mdsymlem1.1	. . . . . . . 8 |- A e. CH
3		chjclt 9324	. . . . . . . 8 |- ((A e. CH /\ p e. CH) -> (A vH p) e. CH)
4	2, 3	mpan 697	. . . . . . 7 |- (p e. CH -> (A vH p) e. CH)
5		mdsymlem1.3	. . . . . . 7 |- C = (A vH p)
6	4, 5	syl5eqel 1555	. . . . . 6 |- (p e. CH -> C e. CH)
7		mdsymlem1.2	. . . . . . 7 |- B e. CH
8		chinclt 9417	. . . . . . 7 |- ((B e. CH /\ C e. CH) -> (B i^i C) e. CH)
9	7, 8	mpan 697	. . . . . 6 |- (C e. CH -> (B i^i C) e. CH)
10	6, 9	syl 10	. . . . 5 |- (p e. CH -> (B i^i C) e. CH)
11		chrelat2t 10292	. . . . . 6 |- (((B i^i C) e. CH /\ A e. CH) -> (-. (B i^i C) (_ A <-> E.r e. Atoms (r (_ (B i^i C) /\ -. r (_ A)))
12	2, 11	mpan2 698	. . . . 5 |- ((B i^i C) e. CH -> (-. (B i^i C) (_ A <-> E.r e. Atoms (r (_ (B i^i C) /\ -. r (_ A)))
13	1, 10, 12	3syl 20	. . . 4 |- (p e. Atoms -> (-. (B i^i C) (_ A <-> E.r e. Atoms (r (_ (B i^i C) /\ -. r (_ A)))
14	13	biimpa 418	. . 3 |- ((p e. Atoms /\ -. (B i^i C) (_ A) -> E.r e. Atoms (r (_ (B i^i C) /\ -. r (_ A))
15	14	ad2antrr 406	. 2 |- ((((p e. Atoms /\ -. (B i^i C) (_ A) /\ p (_ (A vH B)) /\ A =/= 0H) -> E.r e. Atoms (r (_ (B i^i C) /\ -. r (_ A))
16	2	atcvat4 10319	. . . . . . . . . . . . . . 15 |- ((r e. Atoms /\ p e. Atoms) -> ((A =/= 0H /\ r (_ (A vH p)) -> E.q e. Atoms (q (_ A /\ r (_ (p vH q))))
17	16	exp4b 381	. . . . . . . . . . . . . 14 |- (r e. Atoms -> (p e. Atoms -> (A =/= 0H -> (r (_ (A vH p) -> E.q e. Atoms (q (_ A /\ r (_ (p vH q))))))
18	17	com34 36	. . . . . . . . . . . . 13 |- (r e. Atoms -> (p e. Atoms -> (r (_ (A vH p) -> (A =/= 0H -> E.q e. Atoms (q (_ A /\ r (_ (p vH q))))))
19	18	com23 32	. . . . . . . . . . . 12 |- (r e. Atoms -> (r (_ (A vH p) -> (p e. Atoms -> (A =/= 0H -> E.q e. Atoms (q (_ A /\ r (_ (p vH q))))))
20	19	imp4b 365	. . . . . . . . . . 11 |- ((r e. Atoms /\ r (_ (A vH p)) -> ((p e. Atoms /\ A =/= 0H) -> E.q e. Atoms (q (_ A /\ r (_ (p vH q))))
21		ssin 2235	. . . . . . . . . . . 12 |- ((r (_ B /\ r (_ C) <-> r (_ (B i^i C))
22	5	sseq2i 2089	. . . . . . . . . . . . . 14 |- (r (_ C <-> r (_ (A vH p))
23	22	biimp 151	. . . . . . . . . . . . 13 |- (r (_ C -> r (_ (A vH p))
24	23	adantl 390	. . . . . . . . . . . 12 |- ((r (_ B /\ r (_ C) -> r (_ (A vH p))
25	21, 24	sylbir 201	. . . . . . . . . . 11 |- (r (_ (B i^i C) -> r (_ (A vH p))
26	20, 25	sylan2 453	. . . . . . . . . 10 |- ((r e. Atoms /\ r (_ (B i^i C)) -> ((p e. Atoms /\ A =/= 0H) -> E.q e. Atoms (q (_ A /\ r (_ (p vH q))))
27	26	adantrr 397	. . . . . . . . 9 |- ((r e. Atoms /\ (r (_ (B i^i C) /\ -. r (_ A)) -> ((p e. Atoms /\ A =/= 0H) -> E.q e. Atoms (q (_ A /\ r (_ (p vH q))))
28	27	com12 11	. . . . . . . 8 |- ((p e. Atoms /\ A =/= 0H) -> ((r e. Atoms /\ (r (_ (B i^i C) /\ -. r (_ A)) -> E.q e. Atoms (q (_ A /\ r (_ (p vH q))))
29	28	adantlr 395	. . . . . . 7 |- (((p e. Atoms /\ -. (B i^i C) (_ A) /\ A =/= 0H) -> ((r e. Atoms /\ (r (_ (B i^i C) /\ -. r (_ A)) -> E.q e. Atoms (q (_ A /\ r (_ (p vH q))))
30	29	adantlr 395	. . . . . 6 |- ((((p e. Atoms /\ -. (B i^i C) (_ A) /\ p (_ (A vH B)) /\ A =/= 0H) -> ((r e. Atoms /\ (r (_ (B i^i C) /\ -. r (_ A)) -> E.q e. Atoms (q (_ A /\ r (_ (p vH q))))
31	30	imp 350	. . . . 5 |- (((((p e. Atoms /\ -. (B i^i C) (_ A) /\ p (_ (A vH B)) /\ A =/= 0H) /\ (r e. Atoms /\ (r (_ (B i^i C) /\ -. r (_ A))) -> E.q e. Atoms (q (_ A /\ r (_ (p vH q)))
32		atnem0 10299	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((q e. Atoms /\ r e. Atoms) -> (-. q = r <-> (q i^i r) = 0H))
33	32	ancoms 438	. . . . . . . . . . . . . . . . . . . . . 22 |- ((r e. Atoms /\ q e. Atoms) -> (-. q = r <-> (q i^i r) = 0H))
34		sseq1 2085	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (q = r -> (q (_ A <-> r (_ A))
35	34	biimpcd 155	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (q (_ A -> (q = r -> r (_ A))
36	35	con3d 95	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (q (_ A -> (-. r (_ A -> -. q = r))
37	36	imp 350	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((q (_ A /\ -. r (_ A) -> -. q = r)
38	37	adantrl 396	. . . . . . . . . . . . . . . . . . . . . 22 |- ((q (_ A /\ (r (_ (B i^i C) /\ -. r (_ A)) -> -. q = r)
39	33, 38	syl5bi 208	. . . . . . . . . . . . . . . . . . . . 21 |- ((r e. Atoms /\ q e. Atoms) -> ((q (_ A /\ (r (_ (B i^i C) /\ -. r (_ A)) -> (q i^i r) = 0H))
40	39	adantll 394	. . . . . . . . . . . . . . . . . . . 20 |- (((p e. Atoms /\ r e. Atoms) /\ q e. Atoms) -> ((q (_ A /\ (r (_ (B i^i C) /\ -. r (_ A)) -> (q i^i r) = 0H))
41	40	adantr 391	. . . . . . . . . . . . . . . . . . 19 |- ((((p e. Atoms /\ r e. Atoms) /\ q e. Atoms) /\ r (_ (p vH q)) -> ((q (_ A /\ (r (_ (B i^i C) /\ -. r (_ A)) -> (q i^i r) = 0H))
42		chjcomt 9424	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((p e. CH /\ q e. CH) -> (p vH q) = (q vH p))
43		atelch 10266	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (q e. Atoms -> q e. CH)
44	42, 1, 43	syl2an 456	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((p e. Atoms /\ q e. Atoms) -> (p vH q) = (q vH p))
45	44	adantlr 395	. . . . . . . . . . . . . . . . . . . . . 22 |- (((p e. Atoms /\ r e. Atoms) /\ q e. Atoms) -> (p vH q) = (q vH p))
46	45	sseq2d 2092	. . . . . . . . . . . . . . . . . . . . 21 |- (((p e. Atoms /\ r e. Atoms) /\ q e. Atoms) -> (r (_ (p vH q) <-> r (_ (q vH p)))
47		atexcht 10303	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((q e. CH /\ r e. Atoms /\ p e. Atoms) -> ((r (_ (q vH p) /\ (q i^i r) = 0H) -> p (_ (q vH r)))
48	47, 43	syl3an1 861	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((q e. Atoms /\ r e. Atoms /\ p e. Atoms) -> ((r (_ (q vH p) /\ (q i^i r) = 0H) -> p (_ (q vH r)))
49	48	3com13 840	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((p e. Atoms /\ r e. Atoms /\ q e. Atoms) -> ((r (_ (q vH p) /\ (q i^i r) = 0H) -> p (_ (q vH r)))
50	49	3expa 835	. . . . . . . . . . . . . . . . . . . . . 22 |- (((p e. Atoms /\ r e. Atoms) /\ q e. Atoms) -> ((r (_ (q vH p) /\ (q i^i r) = 0H) -> p (_ (q vH r)))
51	50	exp3a 376	. . . . . . . . . . . . . . . . . . . . 21 |- (((p e. Atoms /\ r e. Atoms) /\ q e. Atoms) -> (r (_ (q vH p) -> ((q i^i r) = 0H -> p (_ (q vH r))))
52	46, 51	sylbid 203	. . . . . . . . . . . . . . . . . . . 20 |- (((p e. Atoms /\ r e. Atoms) /\ q e. Atoms) -> (r (_ (p vH q) -> ((q i^i r) = 0H -> p (_ (q vH r))))
53	52	imp 350	. . . . . . . . . . . . . . . . . . 19 |- ((((p e. Atoms /\ r e. Atoms) /\ q e. Atoms) /\ r (_ (p vH q)) -> ((q i^i r) = 0H -> p (_ (q vH r)))
54	41, 53	syld 27	. . . . . . . . . . . . . . . . . 18 |- ((((p e. Atoms /\ r e. Atoms) /\ q e. Atoms) /\ r (_ (p vH q)) -> ((q (_ A /\ (r (_ (B i^i C) /\ -. r (_ A)) -> p (_ (q vH r)))
55	54	exp3a 376	. . . . . . . . . . . . . . . . 17 |- ((((p e. Atoms /\ r e. Atoms) /\ q e. Atoms) /\ r (_ (p vH q)) -> (q (_ A -> ((r (_ (B i^i C) /\ -. r (_ A) -> p (_ (q vH r))))
56	55	exp31 378	. . . . . . . . . . . . . . . 16 |- ((p e. Atoms /\ r e. Atoms) -> (q e. Atoms -> (r (_ (p vH q) -> (q (_ A -> ((r (_ (B i^i C) /\ -. r (_ A)