Theorem mdsymlem5 10329

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
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 groups:   r,q,C   p,c,q,r,A   B,c,p,q,r

Proof of Theorem mdsymlem5

Step	Hyp	Ref	Expression
1		atnem0 10299	. . . . . . . . . . . . . . . . . . . . . 22 |- ((q e. Atoms /\ p e. Atoms) -> (-. q = p <-> (q i^i p) = 0H))
2	1	anbi2d 618	. . . . . . . . . . . . . . . . . . . . 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 801	. . . . . . . . . . . . . . . . . . . 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		atexcht 10303	. . . . . . . . . . . . . . . . . . . . 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 10266	. . . . . . . . . . . . . . . . . . . . 21 |- (q e. Atoms -> q e. CH)
6	4, 5	syl3an1 861	. . . . . . . . . . . . . . . . . . . 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 203	. . . . . . . . . . . . . . . . . . 19 |- ((q e. Atoms /\ p e. Atoms /\ r e. Atoms) -> ((p (_ (q vH r) /\ -. q = p) -> r (_ (q vH p)))
8	7	exp3a 376	. . . . . . . . . . . . . . . . . 18 |- ((q e. Atoms /\ p e. Atoms /\ r e. Atoms) -> (p (_ (q vH r) -> (-. q = p -> r (_ (q vH p))))
9	8	3com23 841	. . . . . . . . . . . . . . . . 17 |- ((q e. Atoms /\ r e. Atoms /\ p e. Atoms) -> (p (_ (q vH r) -> (-. q = p -> r (_ (q vH p))))
10	9	3expa 835	. . . . . . . . . . . . . . . 16 |- (((q e. Atoms /\ r e. Atoms) /\ p e. Atoms) -> (p (_ (q vH r) -> (-. q = p -> r (_ (q vH p))))
11	10	adantrl 396	. . . . . . . . . . . . . . 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 393	. . . . . . . . . . . . . 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 363	. . . . . . . . . . . . 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 396	. . . . . . . . . . . 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 397	. . . . . . . . . . 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 2075	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((q (_ A /\ A (_ (c vH A)) -> q (_ (c vH A))
17		mdsymlem1.1	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- A e. CH
18		chub2t 9426	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((A e. CH /\ c e. CH) -> A (_ (c vH A))
19	17, 18	mpan 697	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (c e. CH -> A (_ (c vH A))
20	16, 19	sylan2 453	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((q (_ A /\ c e. CH) -> q (_ (c vH A))
21		sstr 2075	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((p (_ c /\ c (_ (c vH A)) -> p (_ (c vH A))
22		chub1t 9425	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((c e. CH /\ A e. CH) -> c (_ (c vH A))
23	17, 22	mpan2 698	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (c e. CH -> c (_ (c vH A))
24	21, 23	sylan2 453	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((p (_ c /\ c e. CH) -> p (_ (c vH A))
25	20, 24	anim12i 333	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((q (_ A /\ c e. CH) /\ (p (_ c /\ c e. CH)) -> (q (_ (c vH A) /\ p (_ (c vH A)))
26	25	anandirs 515	. . . . . . . . . . . . . . . . . . . . . 22 |- (((q (_ A /\ p (_ c) /\ c e. CH) -> (q (_ (c vH A) /\ p (_ (c vH A)))
27	26	ancoms 438	. . . . . . . . . . . . . . . . . . . . 21 |- ((c e. CH /\ (q (_ A /\ p (_ c)) -> (q (_ (c vH A) /\ p (_ (c vH A)))
28	27	adantll 394	. . . . . . . . . . . . . . . . . . . 20 |- ((((q e. CH /\ p e. CH) /\ c e. CH) /\ (q (_ A /\ p (_ c)) -> (q (_ (c vH A) /\ p (_ (c vH A)))
29		chlubt 9427	. . . . . . . . . . . . . . . . . . . . . . 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 9324	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((c e. CH /\ A e. CH) -> (c vH A) e. CH)
31	17, 30	mpan2 698	. . . . . . . . . . . . . . . . . . . . . . 23 |- (c e. CH -> (c vH A) e. CH)
32	29, 31	syl3an3 863	. . . . . . . . . . . . . . . . . . . . . 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 835	. . . . . . . . . . . . . . . . . . . . 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 391	. . . . . . . . . . . . . . . . . . . 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 195	. . . . . . . . . . . . . . . . . . 19 |- ((((q e. CH /\ p e. CH) /\ c e. CH) /\ (q (_ A /\ p (_ c)) -> (q vH p) (_ (c vH A))
36	35	adantrl 396	. . . . . . . . . . . . . . . . . 18 |- ((((q e. CH /\ p e. CH) /\ c e. CH) /\ (A (_ c /\ (q (_ A /\ p (_ c))) -> (q vH p) (_ (c vH A))
37		chlejb2t 9431	. . . . . . . . . . . . . . . . . . . . 21 |- ((A e. CH /\ c e. CH) -> (A (_ c <-> (c vH A) = c))
38	17, 37	mpan 697	. . . . . . . . . . . . . . . . . . . 20 |- (c e. CH -> (A (_ c <-> (c vH A) = c))
39	38	biimpa 418	. . . . . . . . . . . . . . . . . . 19 |- ((c e. CH /\ A (_ c) -> (c vH A) = c)
40	39	ad2ant2lr 412	. . . . . . . . . . . . . . . . . 18 |- ((((q e. CH /\ p e. CH) /\ c e. CH) /\ (A (_ c /\ (q (_ A /\ p (_ c))) -> (c vH A) = c)
41	36, 40	sseqtrd 2100	. . . . . . . . . . . . . . . . 17 |- ((((q e. CH /\ p e. CH) /\ c e. CH) /\ (A (_ c /\ (q (_ A /\ p (_ c))) -> (q vH p) (_ c)
42	41	exp45 388	. . . . . . . . . . . . . . . 16 |- (((q e. CH /\ p e. CH) /\ c e. CH) -> (A (_ c -> (q (_ A -> (p (_ c -> (q vH p) (_ c))))
43	42	anasss 442	. . . . . . . . . . . . . . 15 |- ((q e. CH /\ (p e. CH /\ c e. CH)) -> (A (_ c -> (q (_ A -> (p (_ c -> (q vH p) (_ c))))
44		atelch 10266	. . . . . . . . . . . . . . . . 17 |- (p e. Atoms -> p e. CH)
45	44	anim1i 334	. . . . . . . . . . . . . . . 16 |- ((p e. Atoms /\ c e. CH) -> (p e. CH /\ c e. CH))
46	45	ancoms 438	. . . . . . . . . . . . . . 15 |- ((c e. CH /\ p e. Atoms) -> (p e. CH /\ c e. CH))
47	43, 5, 46	syl2an 456	. . . . . . . . . . . . . 14 |- ((q e. Atoms /\ (c e. CH /\ p e. Atoms)) -> (A (_ c -> (q (_ A -> (p (_ c -> (q vH p) (_ c))))
48	47	adantlr 395	. . . . . . . . . . . . 13 |- (((q e. Atoms /\ r e. Atoms) /\ (c e. CH /\ p e. Atoms)) -> (A (_ c -> (q (_ A -> (p (_ c -> (q vH p) (_ c))))
49		pm3.26 319	. . . . . . . . . . . . . 14 |- ((q (_ A /\ r (_ B) -> q (_ A)
50	49	ad2antlr 407	. . . . . . . . . . . . 13 |- (((p (_ (q vH r) /\ (q (_ A /\ r (_ B)) /\ -. q = p) -> q (_ A)
51	48, 50	syl7 23	. . . . . . . . . . . 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))))
52	51	imp44 371	. . . . . . . . . . 11 |- ((((q e. Atoms /\ r e. Atoms) /\ (c e. CH /\ p e. Atoms)) /\ ((A (_ c /\