Theorem mdexch 10262

Description: An exchange lemma for modular pairs. Lemma 1.6 of [MaedaMaeda] p. 2.

Hypotheses

Ref	Expression
mdexch.1	|- A e. CH
mdexch.2	|- B e. CH
mdexch.3	|- C e. CH

Assertion

Ref	Expression
mdexch	|- ((A MH B /\ C MH (A vH B) /\ (C i^i (A vH B)) (_ A) -> ((C vH A) MH B /\ ((C vH A) i^i B) = (A i^i B)))

Proof of Theorem mdexch

Step	Hyp	Ref	Expression
1		mdexch.3	. . . . . . . . . . . . . . 15 |- C e. CH
2		mdexch.1	. . . . . . . . . . . . . . 15 |- A e. CH
3		chjasst 9456	. . . . . . . . . . . . . . 15 |- ((C e. CH /\ A e. CH /\ x e. CH) -> ((C vH A) vH x) = (C vH (A vH x)))
4	1, 2, 3	mp3an12 906	. . . . . . . . . . . . . 14 |- (x e. CH -> ((C vH A) vH x) = (C vH (A vH x)))
5	1, 2	chjcl 9380	. . . . . . . . . . . . . . 15 |- (C vH A) e. CH
6		chjcomt 9429	. . . . . . . . . . . . . . 15 |- ((x e. CH /\ (C vH A) e. CH) -> (x vH (C vH A)) = ((C vH A) vH x))
7	5, 6	mpan2 696	. . . . . . . . . . . . . 14 |- (x e. CH -> (x vH (C vH A)) = ((C vH A) vH x))
8		chjclt 9329	. . . . . . . . . . . . . . . 16 |- ((A e. CH /\ x e. CH) -> (A vH x) e. CH)
9	2, 8	mpan 695	. . . . . . . . . . . . . . 15 |- (x e. CH -> (A vH x) e. CH)
10		chjcomt 9429	. . . . . . . . . . . . . . . 16 |- (((A vH x) e. CH /\ C e. CH) -> ((A vH x) vH C) = (C vH (A vH x)))
11	1, 10	mpan2 696	. . . . . . . . . . . . . . 15 |- ((A vH x) e. CH -> ((A vH x) vH C) = (C vH (A vH x)))
12	9, 11	syl 10	. . . . . . . . . . . . . 14 |- (x e. CH -> ((A vH x) vH C) = (C vH (A vH x)))
13	4, 7, 12	3eqtr4d 1517	. . . . . . . . . . . . 13 |- (x e. CH -> (x vH (C vH A)) = ((A vH x) vH C))
14	13	ineq1d 2216	. . . . . . . . . . . 12 |- (x e. CH -> ((x vH (C vH A)) i^i B) = (((A vH x) vH C) i^i B))
15		inass 2223	. . . . . . . . . . . . 13 |- ((((A vH x) vH C) i^i (A vH B)) i^i B) = (((A vH x) vH C) i^i ((A vH B) i^i B))
16		incom 2208	. . . . . . . . . . . . . . 15 |- ((A vH B) i^i B) = (B i^i (A vH B))
17		mdexch.2	. . . . . . . . . . . . . . . . 17 |- B e. CH
18	2, 17	chjcom 9391	. . . . . . . . . . . . . . . 16 |- (A vH B) = (B vH A)
19	18	ineq2i 2214	. . . . . . . . . . . . . . 15 |- (B i^i (A vH B)) = (B i^i (B vH A))
20	17, 2	chabs2 9442	. . . . . . . . . . . . . . 15 |- (B i^i (B vH A)) = B
21	16, 19, 20	3eqtr 1499	. . . . . . . . . . . . . 14 |- ((A vH B) i^i B) = B
22	21	ineq2i 2214	. . . . . . . . . . . . 13 |- (((A vH x) vH C) i^i ((A vH B) i^i B)) = (((A vH x) vH C) i^i B)
23	15, 22	eqtr 1495	. . . . . . . . . . . 12 |- ((((A vH x) vH C) i^i (A vH B)) i^i B) = (((A vH x) vH C) i^i B)
24	14, 23	syl6eqr 1525	. . . . . . . . . . 11 |- (x e. CH -> ((x vH (C vH A)) i^i B) = ((((A vH x) vH C) i^i (A vH B)) i^i B))
25	24	ad2antrr 404	. . . . . . . . . 10 |- (((x e. CH /\ x (_ B) /\ (C MH (A vH B) /\ (C i^i (A vH B)) (_ A)) -> ((x vH (C vH A)) i^i B) = ((((A vH x) vH C) i^i (A vH B)) i^i B))
26		chlej2t 9434	. . . . . . . . . . . . . . . . 17 |- (((x e. CH /\ B e. CH /\ A e. CH) /\ x (_ B) -> (A vH x) (_ (A vH B))
27	26	ex 373	. . . . . . . . . . . . . . . 16 |- ((x e. CH /\ B e. CH /\ A e. CH) -> (x (_ B -> (A vH x) (_ (A vH B)))
28	17, 2, 27	mp3an23 908	. . . . . . . . . . . . . . 15 |- (x e. CH -> (x (_ B -> (A vH x) (_ (A vH B)))
29	2, 17	chjcl 9380	. . . . . . . . . . . . . . . . . 18 |- (A vH B) e. CH
30		mdit 10222	. . . . . . . . . . . . . . . . . . 19 |- (((C e. CH /\ (A vH B) e. CH /\ (A vH x) e. CH) /\ (C MH (A vH B) /\ (A vH x) (_ (A vH B))) -> (((A vH x) vH C) i^i (A vH B)) = ((A vH x) vH (C i^i (A vH B))))
31	30	exp32 377	. . . . . . . . . . . . . . . . . 18 |- ((C e. CH /\ (A vH B) e. CH /\ (A vH x) e. CH) -> (C MH (A vH B) -> ((A vH x) (_ (A vH B) -> (((A vH x) vH C) i^i (A vH B)) = ((A vH x) vH (C i^i (A vH B))))))
32	1, 29, 31	mp3an12 906	. . . . . . . . . . . . . . . . 17 |- ((A vH x) e. CH -> (C MH (A vH B) -> ((A vH x) (_ (A vH B) -> (((A vH x) vH C) i^i (A vH B)) = ((A vH x) vH (C i^i (A vH B))))))
33	9, 32	syl 10	. . . . . . . . . . . . . . . 16 |- (x e. CH -> (C MH (A vH B) -> ((A vH x) (_ (A vH B) -> (((A vH x) vH C) i^i (A vH B)) = ((A vH x) vH (C i^i (A vH B))))))
34	33	com23 32	. . . . . . . . . . . . . . 15 |- (x e. CH -> ((A vH x) (_ (A vH B) -> (C MH (A vH B) -> (((A vH x) vH C) i^i (A vH B)) = ((A vH x) vH (C i^i (A vH B))))))
35	28, 34	syld 27	. . . . . . . . . . . . . 14 |- (x e. CH -> (x (_ B -> (C MH (A vH B) -> (((A vH x) vH C) i^i (A vH B)) = ((A vH x) vH (C i^i (A vH B))))))
36	35	imp31 362	. . . . . . . . . . . . 13 |- (((x e. CH /\ x (_ B) /\ C MH (A vH B)) -> (((A vH x) vH C) i^i (A vH B)) = ((A vH x) vH (C i^i (A vH B))))
37	36	adantrr 395	. . . . . . . . . . . 12 |- (((x e. CH /\ x (_ B) /\ (C MH (A vH B) /\ (C i^i (A vH B)) (_ A)) -> (((A vH x) vH C) i^i (A vH B)) = ((A vH x) vH (C i^i (A vH B))))
38	1, 29	chincl 9383	. . . . . . . . . . . . . . . . 17 |- (C i^i (A vH B)) e. CH
39		chlej2t 9434	. . . . . . . . . . . . . . . . . 18 |- ((((C i^i (A vH B)) e. CH /\ A e. CH /\ (A vH x) e. CH) /\ (C i^i (A vH B)) (_ A) -> ((A vH x) vH (C i^i (A vH B))) (_ ((A vH x) vH A))
40	39	ex 373	. . . . . . . . . . . . . . . . 17 |- (((C i^i (A vH B)) e. CH /\ A e. CH /\ (A vH x) e. CH) -> ((C i^i (A vH B)) (_ A -> ((A vH x) vH (C i^i (A vH B))) (_ ((A vH x) vH A)))
41	38, 2, 40	mp3an12 906	. . . . . . . . . . . . . . . 16 |- ((A vH x) e. CH -> ((C i^i (A vH B)) (_ A -> ((A vH x) vH (C i^i (A vH B))) (_ ((A vH x) vH A)))
42	9, 41	syl 10	. . . . . . . . . . . . . . 15 |- (x e. CH -> ((C i^i (A vH B)) (_ A -> ((A vH x) vH (C i^i (A vH B))) (_ ((A vH x) vH A)))
43	42	imp 350	. . . . . . . . . . . . . 14 |- ((x e. CH /\ (C i^i (A vH B)) (_ A) -> ((A vH x) vH (C i^i (A vH B))) (_ ((A vH x) vH A))
44		chjcomt 9429	. . . . . . . . . . . . . . . . . 18 |- (((A vH x) e. CH /\ A e. CH) -> ((A vH x) vH A) = (A vH (A vH x)))
45	2, 44	mpan2 696	. . . . . . . . . . . . . . . . 17 |- ((A vH x) e. CH -> ((A vH x) vH A) = (A vH (A vH x)))
46	9, 45	syl 10	. . . . . . . . . . . . . . . 16 |- (x e. CH -> ((A vH x) vH A) = (A vH (A vH x)))
47		chjasst 9456	. . . . . . . . . . . . . . . . . 18 |- ((A e. CH /\ A e. CH /\ x e. CH) -> ((A vH A) vH x) = (A vH (A vH x)))
48	2, 2, 47	mp3an12 906	. . . . . . . . . . . . . . . . 17 |- (x e. CH -> ((A vH A) vH x) = (A vH (A vH x)))
49	2	chjidm 9444	. . . . . . . . . . . . . . . . . 18 |- (A vH A) = A
50	49	opreq1i 3971	. . . . . . . . . . . . . . . . 17 |- ((A vH A) vH x) = (A vH x)
51	48, 50	syl5reqr 1522	. . . . . . . . . . . . . . . 16 |- (x e. CH -> (A vH (A vH x)) = (A vH x))
52		chjcomt 9429	. . . . . . . . . . . . . . . . 17 |- ((A e. CH /\ x e. CH) -> (A vH x) = (x vH A))
53	2, 52	mpan 695	. . . . . . . . . . . . . . . 16 |- (x e. CH -> (A vH x) = (x vH A))
54	46, 51, 53	3eqtrd 1511	. . . . . . . . . . . . . . 15 |- (x e. CH -> ((A vH x) vH A) = (x vH A))
55	54	adantr 389	. . . . . . . . . . . . . 14 |- ((x e. CH /\ (C i^i (A vH B)) (_ A) -> ((A vH x) vH A) = (x vH A))
56	43, 55	sseqtrd 2097	. . . . . . . . . . . . 13 |- ((x e. CH /\ (C i^i (A vH B)) (_ A) -> ((A vH x) vH (C i^i (A vH B))) (_ (x vH A))
57	56	ad2ant2rl 411	. . . . . . . . . . . 12 |- (((x e. CH