Theorem mdsl0 10237

Description: A sublattice condition that transfers the modular pair property. Exercise 12 of [Kalmbach] p. 103. Also Lemma 1.5.3 of [MaedaMaeda] p. 2.

Assertion

Ref	Expression
mdsl0	|- (((A e. CH /\ B e. CH) /\ (C e. CH /\ D e. CH)) -> ((((C (_ A /\ D (_ B) /\ (A i^i B) = 0H) /\ A MH B) -> C MH D))

Proof of Theorem mdsl0

Step	Hyp	Ref	Expression
1		sstr2 2071	. . . . . . . . 9 |- (x (_ D -> (D (_ B -> x (_ B))
2	1	com12 11	. . . . . . . 8 |- (D (_ B -> (x (_ D -> x (_ B))
3	2	ad2antlr 405	. . . . . . 7 |- (((C (_ A /\ D (_ B) /\ (A i^i B) = 0H) -> (x (_ D -> x (_ B))
4	3	ad2antlr 405	. . . . . 6 |- (((((A e. CH /\ B e. CH) /\ (C e. CH /\ D e. CH)) /\ ((C (_ A /\ D (_ B) /\ (A i^i B) = 0H)) /\ x e. CH) -> (x (_ D -> x (_ B))
5		sstr2 2071	. . . . . . . . . 10 |- (((x vH C) i^i D) (_ ((x vH A) i^i B) -> (((x vH A) i^i B) (_ (x vH (A i^i B)) -> ((x vH C) i^i D) (_ (x vH (A i^i B))))
6		sstr2 2071	. . . . . . . . . 10 |- (((x vH C) i^i D) (_ (x vH (A i^i B)) -> ((x vH (A i^i B)) (_ (x vH (C i^i D)) -> ((x vH C) i^i D) (_ (x vH (C i^i D))))
7	5, 6	syl6 22	. . . . . . . . 9 |- (((x vH C) i^i D) (_ ((x vH A) i^i B) -> (((x vH A) i^i B) (_ (x vH (A i^i B)) -> ((x vH (A i^i B)) (_ (x vH (C i^i D)) -> ((x vH C) i^i D) (_ (x vH (C i^i D)))))
8	7	com23 32	. . . . . . . 8 |- (((x vH C) i^i D) (_ ((x vH A) i^i B) -> ((x vH (A i^i B)) (_ (x vH (C i^i D)) -> (((x vH A) i^i B) (_ (x vH (A i^i B)) -> ((x vH C) i^i D) (_ (x vH (C i^i D)))))
9		chlej2t 9434	. . . . . . . . . . . . . . 15 |- (((C e. CH /\ A e. CH /\ x e. CH) /\ C (_ A) -> (x vH C) (_ (x vH A))
10		ss2in 2236	. . . . . . . . . . . . . . . 16 |- (((x vH C) (_ (x vH A) /\ D (_ B) -> ((x vH C) i^i D) (_ ((x vH A) i^i B))
11	10	ex 373	. . . . . . . . . . . . . . 15 |- ((x vH C) (_ (x vH A) -> (D (_ B -> ((x vH C) i^i D) (_ ((x vH A) i^i B)))
12	9, 11	syl 10	. . . . . . . . . . . . . 14 |- (((C e. CH /\ A e. CH /\ x e. CH) /\ C (_ A) -> (D (_ B -> ((x vH C) i^i D) (_ ((x vH A) i^i B)))
13	12	ex 373	. . . . . . . . . . . . 13 |- ((C e. CH /\ A e. CH /\ x e. CH) -> (C (_ A -> (D (_ B -> ((x vH C) i^i D) (_ ((x vH A) i^i B))))
14	13	3expia 835	. . . . . . . . . . . 12 |- ((C e. CH /\ A e. CH) -> (x e. CH -> (C (_ A -> (D (_ B -> ((x vH C) i^i D) (_ ((x vH A) i^i B)))))
15	14	ancoms 436	. . . . . . . . . . 11 |- ((A e. CH /\ C e. CH) -> (x e. CH -> (C (_ A -> (D (_ B -> ((x vH C) i^i D) (_ ((x vH A) i^i B)))))
16	15	ad2ant2r 409	. . . . . . . . . 10 |- (((A e. CH /\ B e. CH) /\ (C e. CH /\ D e. CH)) -> (x e. CH -> (C (_ A -> (D (_ B -> ((x vH C) i^i D) (_ ((x vH A) i^i B)))))
17	16	imp43 370	. . . . . . . . 9 |- (((((A e. CH /\ B e. CH) /\ (C e. CH /\ D e. CH)) /\ x e. CH) /\ (C (_ A /\ D (_ B)) -> ((x vH C) i^i D) (_ ((x vH A) i^i B))
18	17	adantrr 395	. . . . . . . 8 |- (((((A e. CH /\ B e. CH) /\ (C e. CH /\ D e. CH)) /\ x e. CH) /\ ((C (_ A /\ D (_ B) /\ (A i^i B) = 0H)) -> ((x vH C) i^i D) (_ ((x vH A) i^i B))
19		opreq2 3969	. . . . . . . . . . . . . 14 |- ((A i^i B) = 0H -> (x vH (A i^i B)) = (x vH 0H))
20		chj0t 9420	. . . . . . . . . . . . . 14 |- (x e. CH -> (x vH 0H) = x)
21	19, 20	sylan9eqr 1529	. . . . . . . . . . . . 13 |- ((x e. CH /\ (A i^i B) = 0H) -> (x vH (A i^i B)) = x)
22	21	adantl 388	. . . . . . . . . . . 12 |- (((C e. CH /\ D e. CH) /\ (x e. CH /\ (A i^i B) = 0H)) -> (x vH (A i^i B)) = x)
23		chub1t 9430	. . . . . . . . . . . . . . 15 |- ((x e. CH /\ (C i^i D) e. CH) -> x (_ (x vH (C i^i D)))
24	23	ancoms 436	. . . . . . . . . . . . . 14 |- (((C i^i D) e. CH /\ x e. CH) -> x (_ (x vH (C i^i D)))
25		chinclt 9422	. . . . . . . . . . . . . 14 |- ((C e. CH /\ D e. CH) -> (C i^i D) e. CH)
26	24, 25	sylan 448	. . . . . . . . . . . . 13 |- (((C e. CH /\ D e. CH) /\ x e. CH) -> x (_ (x vH (C i^i D)))
27	26	adantrr 395	. . . . . . . . . . . 12 |- (((C e. CH /\ D e. CH) /\ (x e. CH /\ (A i^i B) = 0H)) -> x (_ (x vH (C i^i D)))
28	22, 27	eqsstrd 2095	. . . . . . . . . . 11 |- (((C e. CH /\ D e. CH) /\ (x e. CH /\ (A i^i B) = 0H)) -> (x vH (A i^i B)) (_ (x vH (C i^i D)))
29	28	adantll 392	. . . . . . . . . 10 |- ((((A e. CH /\ B e. CH) /\ (C e. CH /\ D e. CH)) /\ (x e. CH /\ (A i^i B) = 0H)) -> (x vH (A i^i B)) (_ (x vH (C i^i D)))
30	29	anassrs 441	. . . . . . . . 9 |- (((((A e. CH /\ B e. CH) /\ (C e. CH /\ D e. CH)) /\ x e. CH) /\ (A i^i B) = 0H) -> (x vH (A i^i B)) (_ (x vH (C i^i D)))
31	30	adantrl 394	. . . . . . . 8 |- (((((A e. CH /\ B e. CH) /\ (C e. CH /\ D e. CH)) /\ x e. CH) /\ ((C (_ A /\ D (_ B) /\ (A i^i B) = 0H)) -> (x vH (A i^i B)) (_ (x vH (C i^i D)))
32	8, 18, 31	sylc 68	. . . . . . 7 |- (((((A e. CH /\ B e. CH) /\ (C e. CH /\ D e. CH)) /\ x e. CH) /\ ((C (_ A /\ D (_ B) /\ (A i^i B) = 0H)) -> (((x vH A) i^i B) (_ (x vH (A i^i B)) -> ((x vH C) i^i D) (_ (x vH (C i^i D))))
33	32	an1rs 489	. . . . . 6 |- (((((A e. CH /\ B e. CH) /\ (C e. CH /\ D e. CH)) /\ ((C (_ A /\ D (_ B) /\ (A i^i B) = 0H)) /\ x e. CH) -> (((x vH A) i^i B) (_ (x vH (A i^i B)) -> ((x vH C) i^i D) (_ (x vH (C i^i D))))
34	4, 33	imim12d 29	. . . . 5 |- (((((A e. CH /\ B e. CH) /\ (C e. CH /\ D e. CH)) /\ ((C (_ A /\ D (_ B) /\ (A i^i B) = 0H)) /\ x e. CH) -> ((x (_ B -> ((x vH A) i^i B) (_ (x vH (A i^i B))) -> (x (_ D -> ((x vH C) i^i D) (_ (x vH (C i^i D)))))
35	34	r19.20dva 1709	. . . 4 |- ((((A e. CH /\ B e. CH) /\ (C e. CH /\ D e. CH)) /\ ((C (_ A /\ D (_ B) /\ (A i^i B) = 0H)) -> (A.x e. CH (x (_ B -> ((x vH A) i^i B) (_ (x vH (A i^i B))) -> A.x e. CH (x (_ D -> ((x vH C) i^i D) (_ (x vH (C i^i D)))))
36		mdbr2 10223	. . . . 5 |- ((A e. CH /\ B e. CH) -> (A MH B <-> A.x e. CH (x (_ B -> ((x vH A) i^i B) (_ (x vH (A i^i B)))))
37	36	ad2antrr 404	. . . 4 |- ((((A e. CH /\ B e. CH) /\ (C e. CH /\ D e. CH)) /\ ((C (_ A /\ D (_ B) /\ (A i^i B) = 0H)) -> (A MH B <-> A.x e. CH (x (_ B -> ((x vH A) i^i B) (_ (x vH (A i^i B)))))
38		mdbr2 10223	. . . . 5 |- ((C e. CH /\ D e. CH) -> (C MH D <-> A.x e. CH (x (_ D -> ((x vH C) i^i D) (_ (x vH (C i^i D)))))
39	38	ad2antlr 405	. . . 4 |- ((((A e. CH /\ B e. CH) /\ (C e. CH /\ D e. CH