Theorem mdsymlem3 5778

Description: Lemma for mdsym 5784.

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 group(s):   q,r,C   p,q,r,A   B,p,q,r

Proof of Theorem mdsymlem3

Step	Hyp	Ref	Expression
1		atelch 5742	. . . . 5 |- (p e. Atoms -> p e. CH)
2		mdsymlem1.3	. . . . . . . 8 |- C = (A vH p)
3	2	a1i 7	. . . . . . 7 |- (p e. CH -> C = (A vH p))
4		mdsymlem1.1	. . . . . . . 8 |- A e. CH
5		chjclt 5330	. . . . . . . 8 |- ((A e. CH /\ p e. CH) -> (A vH p) e. CH)
6	4, 5	mpan 518	. . . . . . 7 |- (p e. CH -> (A vH p) e. CH)
7	3, 6	eqeltrd 1163	. . . . . 6 |- (p e. CH -> C e. CH)
8		mdsymlem1.2	. . . . . . 7 |- B e. CH
9		chinclt 5416	. . . . . . 7 |- ((B e. CH /\ C e. CH) -> (B i^i C) e. CH)
10	8, 9	mpan 518	. . . . . 6 |- (C e. CH -> (B i^i C) e. CH)
11	7, 10	syl 12	. . . . 5 |- (p e. CH -> (B i^i C) e. CH)
12		chrelat2t 5761	. . . . . 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)))
13	4, 12	mpan2 519	. . . . 5 |- ((B i^i C) e. CH -> (-. (B i^i C) (_ A <-> E.r e. Atoms (r (_ (B i^i C) /\ -. r (_ A)))
14	1, 11, 13	3syl 21	. . . 4 |- (p e. Atoms -> (-. (B i^i C) (_ A <-> E.r e. Atoms (r (_ (B i^i C) /\ -. r (_ A)))
15	14	biimpa 324	. . 3 |- ((p e. Atoms /\ -. (B i^i C) (_ A) -> E.r e. Atoms (r (_ (B i^i C) /\ -. r (_ A))
16	15	ad2antll 320	. 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))
17	4	atcvat4 5775	. . . . . . . . . . . . . . 15 |- ((r e. Atoms /\ p e. Atoms) -> ((-. A = 0H /\ r (_ (A vH p)) -> E.q e. Atoms (q (_ A /\ r (_ (p vH q))))
18	17	exp4b 296	. . . . . . . . . . . . . 14 |- (r e. Atoms -> (p e. Atoms -> (-. A = 0H -> (r (_ (A vH p) -> E.q e. Atoms (q (_ A /\ r (_ (p vH q))))))
19	18	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))))))
20	19	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))))))
21	20	imp4b 283	. . . . . . . . . . 11 |- ((r e. Atoms /\ r (_ (A vH p)) -> ((p e. Atoms /\ -. A = 0H) -> E.q e. Atoms (q (_ A /\ r (_ (p vH q))))
22		ssin 1659	. . . . . . . . . . . 12 |- ((r (_ B /\ r (_ C) <-> r (_ (B i^i C))
23	2	sseq2i 1525	. . . . . . . . . . . . . 14 |- (r (_ C <-> r (_ (A vH p))
24	23	biimp 133	. . . . . . . . . . . . 13 |- (r (_ C -> r (_ (A vH p))
25	24	adantl 305	. . . . . . . . . . . 12 |- ((r (_ B /\ r (_ C) -> r (_ (A vH p))
26	22, 25	sylbir 176	. . . . . . . . . . 11 |- (r (_ (B i^i C) -> r (_ (A vH p))
27	21, 26	sylan2 346	. . . . . . . . . 10 |- ((r e. Atoms /\ r (_ (B i^i C)) -> ((p e. Atoms /\ -. A = 0H) -> E.q e. Atoms (q (_ A /\ r (_ (p vH q))))
28	27	adantrr 312	. . . . . . . . 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))))
29	28	com12 13	. . . . . . . 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))))
30	29	adantlr 310	. . . . . . 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))))
31	30	adantlr 310	. . . . . 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))))
32	31	imp 277	. . . . 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)))
33		atnem0 5766	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((q e. Atoms /\ r e. Atoms) -> (-. q = r <-> (q i^i r) = 0H))
34	33	ancoms 334	. . . . . . . . . . . . . . . . . . . . . 22 |- ((r e. Atoms /\ q e. Atoms) -> (-. q = r <-> (q i^i r) = 0H))
35		sseq1 1521	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (q = r -> (q (_ A <-> r (_ A))
36	35	biimpcd 137	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (q (_ A -> (q = r -> r (_ A))
37	36	con3d 87	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (q (_ A -> (-. r (_ A -> -. q = r))
38	37	imp 277	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((q (_ A /\ -. r (_ A) -> -. q = r)
39	38	adantrl 311	. . . . . . . . . . . . . . . . . . . . . 22 |- ((q (_ A /\ (r (_ (B i^i C) /\ -. r (_ A)) -> -. q = r)
40	34, 39	syl5bi 183	. . . . . . . . . . . . . . . . . . . . 21 |- ((r e. Atoms /\ q e. Atoms) -> ((q (_ A /\ (r (_ (B i^i C) /\ -. r (_ A)) -> (q i^i r) = 0H))
41	40	adantll 309	. . . . . . . . . . . . . . . . . . . 20 |- (((p e. Atoms /\ r e. Atoms) /\ q e. Atoms) -> ((q (_ A /\ (r (_ (B i^i C) /\ -. r (_ A)) -> (q i^i r) = 0H))
42	41	adantr 306	. . . . . . . . . . . . . . . . . . 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))
43		chjcomt 5423	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((p e. CH /\ q e. CH) -> (p vH q) = (q vH p))
44		atelch 5742	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (q e. Atoms -> q e. CH)
45	43, 1, 44	syl2an 349	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((p e. Atoms /\ q e. Atoms) -> (p vH q) = (q vH p))
46	45	adantlr 310	. . . . . . . . . . . . . . . . . . . . . 22 |- (((p e. Atoms /\ r e. Atoms) /\ q e. Atoms) -> (p vH q) = (q vH p))
47	46	sseq2d 1528	. . . . . . . . . . . . . . . . . . . . 21 |- (((p e. Atoms /\ r e. Atoms) /\ q e. Atoms) -> (r (_ (p vH q) <-> r (_ (q vH p)))
48		atexch 5769	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((q e. CH /\ r e. Atoms /\ p e. Atoms) -> ((r (_ (q vH p) /\ (q i^i r) = 0H) -> p (_ (q vH r)))
49	48, 44	syl3an1 619	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((q e. Atoms /\ r e. Atoms /\ p e. Atoms) -> ((r (_ (q vH p) /\ (q i^i r) = 0H) -> p (_ (q vH r)))
50	49	3com13 615	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((p e. Atoms /\ r e. Atoms /\ q e. Atoms) -> ((r (_ (q vH p) /\ (q i^i r) = 0H) -> p (_ (q vH r)))
51	50	3expa 612	. . . . . . . . . . . . . . . . . . . . . 22 |- (((p e. Atoms /\ r e. Atoms) /\ q e. Atoms) -> ((r (_ (q vH p) /\ (q i^i r) = 0H) -> p (_ (q vH r)))
52	51	exp3a 292	. . . . . . . . . . . . . . . . . . . . 21 |- (((p e. Atoms /\ r e. Atoms) /\ q e. Atoms) -> (r (_ (q vH p) -> ((q i^i r) = 0H -> p (_ (q vH r))))
53	47, 52	sylbid 178	. . . . . . . . . . . . . . . . . . . 20 |- (((p e. Atoms /\ r e. Atoms) /\ q e. Atoms) -> (r (_ (p vH q) -> ((q i^i r) = 0H -> p (_ (q vH r))))
54	53	imp 277	. . . . . . . . . . . . . . . . . . 19 |- ((((p e. Atoms /\ r e. Atoms) /\ q e. Atoms) /\ r (_ (p vH q)) -> ((q i^i r) = 0H -> p (_ (q vH r)))
55	42, 54	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)))
56	55	exp3a 292	. . . . . . . . . . . . . . . . 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))))
57	56	exp31 293	. . . . . . . . . . . . . . . 16 |- ((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))))))
58	57	com24 37	. . . . . . . . . . . . . . 15 |- ((p e. Atoms <