Theorem mdsymlem5 5780

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
mdsymlem5	|- ((q e. Atoms /\ r e. Atoms) -> (-. q = p -> ((p (_ (q vH r) /\ (q (_ A /\ r (_ B)) -> (((c e. CH /\ A (_ c) /\ p e. Atoms) -> (p (_ c -> p (_ ((c i^i B) vH A))))))

Distinct variable group(s):   q,r,C   c,p,q,r,A   B,c,p,q,r

Proof of Theorem mdsymlem5

Step	Hyp	Ref	Expression
1		atnem0 5766	. . . . . . . . . . . . . . . . . . . . . 22 |- ((q e. Atoms /\ p e. Atoms) -> (-. q = p <-> (q i^i p) = 0H))
2	1	anbi2d 468	. . . . . . . . . . . . . . . . . . . . 21 |- ((q e. Atoms /\ p e. Atoms) -> ((p (_ (q vH r) /\ -. q = p) <-> (p (_ (q vH r) /\ (q i^i p) = 0H)))
3	2	3adant3 599	. . . . . . . . . . . . . . . . . . . 20 |- ((q e. Atoms /\ p e. Atoms /\ r e. Atoms) -> ((p (_ (q vH r) /\ -. q = p) <-> (p (_ (q vH r) /\ (q i^i p) = 0H)))
4		atexch 5769	. . . . . . . . . . . . . . . . . . . . 21 |- ((q e. CH /\ p e. Atoms /\ r e. Atoms) -> ((p (_ (q vH r) /\ (q i^i p) = 0H) -> r (_ (q vH p)))
5		atelch 5742	. . . . . . . . . . . . . . . . . . . . 21 |- (q e. Atoms -> q e. CH)
6	4, 5	syl3an1 619	. . . . . . . . . . . . . . . . . . . 20 |- ((q e. Atoms /\ p e. Atoms /\ r e. Atoms) -> ((p (_ (q vH r) /\ (q i^i p) = 0H) -> r (_ (q vH p)))
7	3, 6	sylbid 178	. . . . . . . . . . . . . . . . . . 19 |- ((q e. Atoms /\ p e. Atoms /\ r e. Atoms) -> ((p (_ (q vH r) /\ -. q = p) -> r (_ (q vH p)))
8	7	exp3a 292	. . . . . . . . . . . . . . . . . 18 |- ((q e. Atoms /\ p e. Atoms /\ r e. Atoms) -> (p (_ (q vH r) -> (-. q = p -> r (_ (q vH p))))
9	8	3com23 616	. . . . . . . . . . . . . . . . 17 |- ((q e. Atoms /\ r e. Atoms /\ p e. Atoms) -> (p (_ (q vH r) -> (-. q = p -> r (_ (q vH p))))
10	9	3expa 612	. . . . . . . . . . . . . . . 16 |- (((q e. Atoms /\ r e. Atoms) /\ p e. Atoms) -> (p (_ (q vH r) -> (-. q = p -> r (_ (q vH p))))
11	10	adantrl 311	. . . . . . . . . . . . . . 15 |- (((q e. Atoms /\ r e. Atoms) /\ (c e. CH /\ p e. Atoms)) -> (p (_ (q vH r) -> (-. q = p -> r (_ (q vH p))))
12	11	adantrd 308	. . . . . . . . . . . . . 14 |- (((q e. Atoms /\ r e. Atoms) /\ (c e. CH /\ p e. Atoms)) -> ((p (_ (q vH r) /\ (q (_ A /\ r (_ B)) -> (-. q = p -> r (_ (q vH p))))
13	12	imp32 281	. . . . . . . . . . . . 13 |- ((((q e. Atoms /\ r e. Atoms) /\ (c e. CH /\ p e. Atoms)) /\ ((p (_ (q vH r) /\ (q (_ A /\ r (_ B)) /\ -. q = p)) -> r (_ (q vH p))
14	13	adantrl 311	. . . . . . . . . . . 12 |- ((((q e. Atoms /\ r e. Atoms) /\ (c e. CH /\ p e. Atoms)) /\ (A (_ c /\ ((p (_ (q vH r) /\ (q (_ A /\ r (_ B)) /\ -. q = p))) -> r (_ (q vH p))
15	14	adantrr 312	. . . . . . . . . . 11 |- ((((q e. Atoms /\ r e. Atoms) /\ (c e. CH /\ p e. Atoms)) /\ ((A (_ c /\ ((p (_ (q vH r) /\ (q (_ A /\ r (_ B)) /\ -. q = p)) /\ p (_ c)) -> r (_ (q vH p))
16		sstr 1511	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((q (_ A /\ A (_ (c vH A)) -> q (_ (c vH A))
17		mdsymlem1.1	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- A e. CH
18		chub2t 5425	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((A e. CH /\ c e. CH) -> A (_ (c vH A))
19	17, 18	mpan 518	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (c e. CH -> A (_ (c vH A))
20	16, 19	sylan2 346	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((q (_ A /\ c e. CH) -> q (_ (c vH A))
21		sstr 1511	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((p (_ c /\ c (_ (c vH A)) -> p (_ (c vH A))
22		chub1t 5424	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((c e. CH /\ A e. CH) -> c (_ (c vH A))
23	17, 22	mpan2 519	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (c e. CH -> c (_ (c vH A))
24	21, 23	sylan2 346	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((p (_ c /\ c e. CH) -> p (_ (c vH A))
25	20, 24	anim12i 268	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((q (_ A /\ c e. CH) /\ (p (_ c /\ c e. CH)) -> (q (_ (c vH A) /\ p (_ (c vH A)))
26	25	anandirs 395	. . . . . . . . . . . . . . . . . . . . . 22 |- (((q (_ A /\ p (_ c) /\ c e. CH) -> (q (_ (c vH A) /\ p (_ (c vH A)))
27	26	ancoms 334	. . . . . . . . . . . . . . . . . . . . 21 |- ((c e. CH /\ (q (_ A /\ p (_ c)) -> (q (_ (c vH A) /\ p (_ (c vH A)))
28	27	adantll 309	. . . . . . . . . . . . . . . . . . . 20 |- ((((q e. CH /\ p e. CH) /\ c e. CH) /\ (q (_ A /\ p (_ c)) -> (q (_ (c vH A) /\ p (_ (c vH A)))
29		chlubt 5426	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((q e. CH /\ p e. CH /\ (c vH A) e. CH) -> ((q (_ (c vH A) /\ p (_ (c vH A)) <-> (q vH p) (_ (c vH A)))
30		chjclt 5330	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((c e. CH /\ A e. CH) -> (c vH A) e. CH)
31	17, 30	mpan2 519	. . . . . . . . . . . . . . . . . . . . . . 23 |- (c e. CH -> (c vH A) e. CH)
32	29, 31	syl3an3 621	. . . . . . . . . . . . . . . . . . . . . 22 |- ((q e. CH /\ p e. CH /\ c e. CH) -> ((q (_ (c vH A) /\ p (_ (c vH A)) <-> (q vH p) (_ (c vH A)))
33	32	3expa 612	. . . . . . . . . . . . . . . . . . . . 21 |- (((q e. CH /\ p e. CH) /\ c e. CH) -> ((q (_ (c vH A) /\ p (_ (c vH A)) <-> (q vH p) (_ (c vH A)))
34	33	adantr 306	. . . . . . . . . . . . . . . . . . . 20 |- ((((q e. CH /\ p e. CH) /\ c e. CH) /\ (q (_ A /\ p (_ c)) -> ((q (_ (c vH A) /\ p (_ (c vH A)) <-> (q vH p) (_ (c vH A)))
35	28, 34	mpbid 170	. . . . . . . . . . . . . . . . . . 19 |- ((((q e. CH /\ p e. CH) /\ c e. CH) /\ (q (_ A /\ p (_ c)) -> (q vH p) (_ (c vH A))
36	35	adantrl 311	. . . . . . . . . . . . . . . . . 18 |- ((((q e. CH /\ p e. CH) /\ c e. CH) /\ (A (_ c /\ (q (_ A /\ p (_ c))) -> (q vH p) (_ (c vH A))
37		chlejb2t 5430	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A e. CH /\ c e. CH) -> (A (_ c <-> (c vH A) = c))
38	17, 37	mpan 518	. . . . . . . . . . . . . . . . . . . . 21 |- (c e. CH -> (A (_ c <-> (c vH A) = c))
39	38	biimpa 324	. . . . . . . . . . . . . . . . . . . 20 |- ((c e. CH /\ A (_ c) -> (c vH A) = c)
40	39	adantll 309	. . . . . . . . . . . . . . . . . . 19 |- ((((q e. CH /\ p e. CH) /\ c e. CH) /\ A (_ c) -> (c vH A) = c)
41	40	adantrr 312	. . . . . . . . . . . . . . . . . 18 |- ((((q e. CH /\ p e. CH) /\ c e. CH) /\ (A (_ c /\ (q (_ A /\ p (_ c))) -> (c vH A) = c)
42	36, 41	sseqtrd 1536	. . . . . . . . . . . . . . . . 17 |- ((((q e. CH /\ p e. CH) /\ c e. CH) /\ (A (_ c /\ (q (_ A /\ p (_ c))) -> (q vH p) (_ c)
43	42	exp45 303	. . . . . . . . . . . . . . . 16 |- (((q e. CH /\ p e. CH) /\ c e. CH) -> (A (_ c -> (q (_ A -> (p (_ c -> (q vH p) (_ c))))
44	43	anasss 337	. . . . . . . . . . . . . . 15 |- ((q e. CH /\ (p e. CH /\ c e. CH)) -> (A (_ c -> (q (_ A -> (p (_ c -> (q vH p) (_ c))))
45		atelch 5742	. . . . . . . . . . . . . . . . 17 |- (p e. Atoms -> p e. CH)
46	45	anim1i 269	. . . . . . . . . . . . . . . 16 |- ((p e. Atoms /\ c e. CH) -> (p e. CH /\ c e. CH))
47	46	ancoms 334	. . . . . . . . . . . . . . 15 |- ((c e. CH /\ p e. Atoms) -> (p e. CH /\ c e. CH))
48	44, 5, 47	syl2an 349	. . . . . . . . . . . . . 14 |- ((q e. Atoms /\ (c e. CH /\ p e. Atoms)) -> (A (_ c -> (q (_ A -> (p (_ c -> (q vH p) (_ c))))
49	48	adantlr 310	. . . . . . . . . . . . 13 |- (((q e. Atoms /\ r e. Atoms) /\ (c e. CH /\ p e. Atoms)) -> (A (_ c -> (q (_ A -> (p (_ c -> (q vH p) (_ c))))
50		pm3.26 256	. . . . . . . . . . . . . 14 |- ((q (_ A /\ r (_ B) -> q (_ A)
51	50	ad2antlr 321	. . . . . . . . . . . . 13 |- (((p (_ (q vH r) /\ (q (_ A /\ r (_ B)) /\ -. q = p) -> q (_ A)
52	49, 51	syl7 24	. . . . . . . . . . . 12 |- (((q e. Atoms /\ r e. Atoms) /\ (c e. CH /\ p e. Atoms)) -> (A (_ c -> (((p (_ (q vH r) /\ (q (_ A /\ r (_ B)) /\ -. q = p) -> (p (_ c -> (q vH p) (_ c))))
53	52	imp44 289	. . . . . . . . . . 11 |- ((((q e. Atoms /\ r e. Atoms) /\ (c e. CH /\ p e. Atoms)) /\ ((A (_ c /\ ((p (_ (q vH r) /\ (q (_ A /\ r