Metamath Proof Explorer

Theorem mdexchi

Description: An exchange lemma for modular pairs. Lemma 1.6 of MaedaMaeda p. 2. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypotheses mdexch.1 
|- A e. CH
mdexch.2 
|- B e. CH
mdexch.3 
|- C e. CH
Assertion mdexchi 
|- ( ( A MH B /\ C MH ( A vH B ) /\ ( C i^i ( A vH B ) ) C_ A ) -> ( ( C vH A ) MH B /\ ( ( C vH A ) i^i B ) = ( A i^i B ) ) )

Proof

Step Hyp Ref Expression
1 mdexch.1 
 |-  A e. CH
2 mdexch.2 
 |-  B e. CH
3 mdexch.3 
 |-  C e. CH
4 chjass 
 |-  ( ( C e. CH /\ A e. CH /\ x e. CH ) -> ( ( C vH A ) vH x ) = ( C vH ( A vH x ) ) )
5 3 1 4 mp3an12 
 |-  ( x e. CH -> ( ( C vH A ) vH x ) = ( C vH ( A vH x ) ) )
6 3 1 chjcli 
 |-  ( C vH A ) e. CH
7 chjcom 
 |-  ( ( x e. CH /\ ( C vH A ) e. CH ) -> ( x vH ( C vH A ) ) = ( ( C vH A ) vH x ) )
8 6 7 mpan2 
 |-  ( x e. CH -> ( x vH ( C vH A ) ) = ( ( C vH A ) vH x ) )
9 chjcl 
 |-  ( ( A e. CH /\ x e. CH ) -> ( A vH x ) e. CH )
10 1 9 mpan 
 |-  ( x e. CH -> ( A vH x ) e. CH )
11 chjcom 
 |-  ( ( ( A vH x ) e. CH /\ C e. CH ) -> ( ( A vH x ) vH C ) = ( C vH ( A vH x ) ) )
12 10 3 11 sylancl 
 |-  ( x e. CH -> ( ( A vH x ) vH C ) = ( C vH ( A vH x ) ) )
13 5 8 12 3eqtr4d 
 |-  ( x e. CH -> ( x vH ( C vH A ) ) = ( ( A vH x ) vH C ) )
14 13 ineq1d 
 |-  ( x e. CH -> ( ( x vH ( C vH A ) ) i^i B ) = ( ( ( A vH x ) vH C ) i^i B ) )
15 inass 
 |-  ( ( ( ( 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 
 |-  ( ( A vH B ) i^i B ) = ( B i^i ( A vH B ) )
17 1 2 chjcomi 
 |-  ( A vH B ) = ( B vH A )
18 17 ineq2i 
 |-  ( B i^i ( A vH B ) ) = ( B i^i ( B vH A ) )
19 2 1 chabs2i 
 |-  ( B i^i ( B vH A ) ) = B
20 18 19 eqtri 
 |-  ( B i^i ( A vH B ) ) = B
21 16 20 eqtri 
 |-  ( ( A vH B ) i^i B ) = B
22 21 ineq2i 
 |-  ( ( ( A vH x ) vH C ) i^i ( ( A vH B ) i^i B ) ) = ( ( ( A vH x ) vH C ) i^i B )
23 15 22 eqtri 
 |-  ( ( ( ( A vH x ) vH C ) i^i ( A vH B ) ) i^i B ) = ( ( ( A vH x ) vH C ) i^i B )
24 14 23 eqtr4di 
 |-  ( 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 
 |-  ( ( ( x e. CH /\ x C_ B ) /\ ( C MH ( A vH B ) /\ ( C i^i ( A vH B ) ) C_ A ) ) -> ( ( x vH ( C vH A ) ) i^i B ) = ( ( ( ( A vH x ) vH C ) i^i ( A vH B ) ) i^i B ) )
26 chlej2 
 |-  ( ( ( x e. CH /\ B e. CH /\ A e. CH ) /\ x C_ B ) -> ( A vH x ) C_ ( A vH B ) )
27 26 ex 
 |-  ( ( x e. CH /\ B e. CH /\ A e. CH ) -> ( x C_ B -> ( A vH x ) C_ ( A vH B ) ) )
28 2 1 27 mp3an23 
 |-  ( x e. CH -> ( x C_ B -> ( A vH x ) C_ ( A vH B ) ) )
29 1 2 chjcli 
 |-  ( A vH B ) e. CH
30 mdi 
 |-  ( ( ( C e. CH /\ ( A vH B ) e. CH /\ ( A vH x ) e. CH ) /\ ( C MH ( A vH B ) /\ ( A vH x ) C_ ( 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 
 |-  ( ( C e. CH /\ ( A vH B ) e. CH /\ ( A vH x ) e. CH ) -> ( C MH ( A vH B ) -> ( ( A vH x ) C_ ( A vH B ) -> ( ( ( A vH x ) vH C ) i^i ( A vH B ) ) = ( ( A vH x ) vH ( C i^i ( A vH B ) ) ) ) ) )
32 3 29 31 mp3an12 
 |-  ( ( A vH x ) e. CH -> ( C MH ( A vH B ) -> ( ( A vH x ) C_ ( A vH B ) -> ( ( ( A vH x ) vH C ) i^i ( A vH B ) ) = ( ( A vH x ) vH ( C i^i ( A vH B ) ) ) ) ) )
33 10 32 syl 
 |-  ( x e. CH -> ( C MH ( A vH B ) -> ( ( A vH x ) C_ ( 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 
 |-  ( x e. CH -> ( ( A vH x ) C_ ( 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 
 |-  ( x e. CH -> ( x C_ 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 
 |-  ( ( ( x e. CH /\ x C_ 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 
 |-  ( ( ( x e. CH /\ x C_ B ) /\ ( C MH ( A vH B ) /\ ( C i^i ( A vH B ) ) C_ A ) ) -> ( ( ( A vH x ) vH C ) i^i ( A vH B ) ) = ( ( A vH x ) vH ( C i^i ( A vH B ) ) ) )
38 3 29 chincli 
 |-  ( C i^i ( A vH B ) ) e. CH
39 chlej2 
 |-  ( ( ( ( C i^i ( A vH B ) ) e. CH /\ A e. CH /\ ( A vH x ) e. CH ) /\ ( C i^i ( A vH B ) ) C_ A ) -> ( ( A vH x ) vH ( C i^i ( A vH B ) ) ) C_ ( ( A vH x ) vH A ) )
40 39 ex 
 |-  ( ( ( C i^i ( A vH B ) ) e. CH /\ A e. CH /\ ( A vH x ) e. CH ) -> ( ( C i^i ( A vH B ) ) C_ A -> ( ( A vH x ) vH ( C i^i ( A vH B ) ) ) C_ ( ( A vH x ) vH A ) ) )
41 38 1 40 mp3an12 
 |-  ( ( A vH x ) e. CH -> ( ( C i^i ( A vH B ) ) C_ A -> ( ( A vH x ) vH ( C i^i ( A vH B ) ) ) C_ ( ( A vH x ) vH A ) ) )
42 10 41 syl 
 |-  ( x e. CH -> ( ( C i^i ( A vH B ) ) C_ A -> ( ( A vH x ) vH ( C i^i ( A vH B ) ) ) C_ ( ( A vH x ) vH A ) ) )
43 42 imp 
 |-  ( ( x e. CH /\ ( C i^i ( A vH B ) ) C_ A ) -> ( ( A vH x ) vH ( C i^i ( A vH B ) ) ) C_ ( ( A vH x ) vH A ) )
44 chjcom 
 |-  ( ( ( A vH x ) e. CH /\ A e. CH ) -> ( ( A vH x ) vH A ) = ( A vH ( A vH x ) ) )
45 10 1 44 sylancl 
 |-  ( x e. CH -> ( ( A vH x ) vH A ) = ( A vH ( A vH x ) ) )
46 1 chjidmi 
 |-  ( A vH A ) = A
47 46 oveq1i 
 |-  ( ( A vH A ) vH x ) = ( A vH x )
48 chjass 
 |-  ( ( A e. CH /\ A e. CH /\ x e. CH ) -> ( ( A vH A ) vH x ) = ( A vH ( A vH x ) ) )
49 1 1 48 mp3an12 
 |-  ( x e. CH -> ( ( A vH A ) vH x ) = ( A vH ( A vH x ) ) )
50 chjcom 
 |-  ( ( A e. CH /\ x e. CH ) -> ( A vH x ) = ( x vH A ) )
51 1 50 mpan 
 |-  ( x e. CH -> ( A vH x ) = ( x vH A ) )
52 47 49 51 3eqtr3a 
 |-  ( x e. CH -> ( A vH ( A vH x ) ) = ( x vH A ) )
53 45 52 eqtrd 
 |-  ( x e. CH -> ( ( A vH x ) vH A ) = ( x vH A ) )
54 53 adantr 
 |-  ( ( x e. CH /\ ( C i^i ( A vH B ) ) C_ A ) -> ( ( A vH x ) vH A ) = ( x vH A ) )
55 43 54 sseqtrd 
 |-  ( ( x e. CH /\ ( C i^i ( A vH B ) ) C_ A ) -> ( ( A vH x ) vH ( C i^i ( A vH B ) ) ) C_ ( x vH A ) )
56 55 ad2ant2rl 
 |-  ( ( ( x e. CH /\ x C_ B ) /\ ( C MH ( A vH B ) /\ ( C i^i ( A vH B ) ) C_ A ) ) -> ( ( A vH x ) vH ( C i^i ( A vH B ) ) ) C_ ( x vH A ) )
57 37 56 eqsstrd 
 |-  ( ( ( x e. CH /\ x C_ B ) /\ ( C MH ( A vH B ) /\ ( C i^i ( A vH B ) ) C_ A ) ) -> ( ( ( A vH x ) vH C ) i^i ( A vH B ) ) C_ ( x vH A ) )
58 57 ssrind 
 |-  ( ( ( x e. CH /\ x C_ B ) /\ ( C MH ( A vH B ) /\ ( C i^i ( A vH B ) ) C_ A ) ) -> ( ( ( ( A vH x ) vH C ) i^i ( A vH B ) ) i^i B ) C_ ( ( x vH A ) i^i B ) )
59 25 58 eqsstrd 
 |-  ( ( ( x e. CH /\ x C_ B ) /\ ( C MH ( A vH B ) /\ ( C i^i ( A vH B ) ) C_ A ) ) -> ( ( x vH ( C vH A ) ) i^i B ) C_ ( ( x vH A ) i^i B ) )
60 59 adantrl 
 |-  ( ( ( x e. CH /\ x C_ B ) /\ ( A MH B /\ ( C MH ( A vH B ) /\ ( C i^i ( A vH B ) ) C_ A ) ) ) -> ( ( x vH ( C vH A ) ) i^i B ) C_ ( ( x vH A ) i^i B ) )
61 mdi 
 |-  ( ( ( A e. CH /\ B e. CH /\ x e. CH ) /\ ( A MH B /\ x C_ B ) ) -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) )
62 61 exp32 
 |-  ( ( A e. CH /\ B e. CH /\ x e. CH ) -> ( A MH B -> ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) ) )
63 1 2 62 mp3an12 
 |-  ( x e. CH -> ( A MH B -> ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) ) )
64 63 com23 
 |-  ( x e. CH -> ( x C_ B -> ( A MH B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) ) )
65 64 imp31 
 |-  ( ( ( x e. CH /\ x C_ B ) /\ A MH B ) -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) )
66 1 3 chub2i 
 |-  A C_ ( C vH A )
67 ssrin 
 |-  ( A C_ ( C vH A ) -> ( A i^i B ) C_ ( ( C vH A ) i^i B ) )
68 66 67 ax-mp 
 |-  ( A i^i B ) C_ ( ( C vH A ) i^i B )
69 1 2 chincli 
 |-  ( A i^i B ) e. CH
70 6 2 chincli 
 |-  ( ( C vH A ) i^i B ) e. CH
71 chlej2 
 |-  ( ( ( ( A i^i B ) e. CH /\ ( ( C vH A ) i^i B ) e. CH /\ x e. CH ) /\ ( A i^i B ) C_ ( ( C vH A ) i^i B ) ) -> ( x vH ( A i^i B ) ) C_ ( x vH ( ( C vH A ) i^i B ) ) )
72 71 ex 
 |-  ( ( ( A i^i B ) e. CH /\ ( ( C vH A ) i^i B ) e. CH /\ x e. CH ) -> ( ( A i^i B ) C_ ( ( C vH A ) i^i B ) -> ( x vH ( A i^i B ) ) C_ ( x vH ( ( C vH A ) i^i B ) ) ) )
73 69 70 72 mp3an12 
 |-  ( x e. CH -> ( ( A i^i B ) C_ ( ( C vH A ) i^i B ) -> ( x vH ( A i^i B ) ) C_ ( x vH ( ( C vH A ) i^i B ) ) ) )
74 68 73 mpi 
 |-  ( x e. CH -> ( x vH ( A i^i B ) ) C_ ( x vH ( ( C vH A ) i^i B ) ) )
75 74 ad2antrr 
 |-  ( ( ( x e. CH /\ x C_ B ) /\ A MH B ) -> ( x vH ( A i^i B ) ) C_ ( x vH ( ( C vH A ) i^i B ) ) )
76 65 75 eqsstrd 
 |-  ( ( ( x e. CH /\ x C_ B ) /\ A MH B ) -> ( ( x vH A ) i^i B ) C_ ( x vH ( ( C vH A ) i^i B ) ) )
77 76 adantrr 
 |-  ( ( ( x e. CH /\ x C_ B ) /\ ( A MH B /\ ( C MH ( A vH B ) /\ ( C i^i ( A vH B ) ) C_ A ) ) ) -> ( ( x vH A ) i^i B ) C_ ( x vH ( ( C vH A ) i^i B ) ) )
78 60 77 sstrd 
 |-  ( ( ( x e. CH /\ x C_ B ) /\ ( A MH B /\ ( C MH ( A vH B ) /\ ( C i^i ( A vH B ) ) C_ A ) ) ) -> ( ( x vH ( C vH A ) ) i^i B ) C_ ( x vH ( ( C vH A ) i^i B ) ) )
79 78 exp31 
 |-  ( x e. CH -> ( x C_ B -> ( ( A MH B /\ ( C MH ( A vH B ) /\ ( C i^i ( A vH B ) ) C_ A ) ) -> ( ( x vH ( C vH A ) ) i^i B ) C_ ( x vH ( ( C vH A ) i^i B ) ) ) ) )
80 79 com3r 
 |-  ( ( A MH B /\ ( C MH ( A vH B ) /\ ( C i^i ( A vH B ) ) C_ A ) ) -> ( x e. CH -> ( x C_ B -> ( ( x vH ( C vH A ) ) i^i B ) C_ ( x vH ( ( C vH A ) i^i B ) ) ) ) )
81 80 3impb 
 |-  ( ( A MH B /\ C MH ( A vH B ) /\ ( C i^i ( A vH B ) ) C_ A ) -> ( x e. CH -> ( x C_ B -> ( ( x vH ( C vH A ) ) i^i B ) C_ ( x vH ( ( C vH A ) i^i B ) ) ) ) )
82 81 ralrimiv 
 |-  ( ( A MH B /\ C MH ( A vH B ) /\ ( C i^i ( A vH B ) ) C_ A ) -> A. x e. CH ( x C_ B -> ( ( x vH ( C vH A ) ) i^i B ) C_ ( x vH ( ( C vH A ) i^i B ) ) ) )
83 mdbr2 
 |-  ( ( ( C vH A ) e. CH /\ B e. CH ) -> ( ( C vH A ) MH B <-> A. x e. CH ( x C_ B -> ( ( x vH ( C vH A ) ) i^i B ) C_ ( x vH ( ( C vH A ) i^i B ) ) ) ) )
84 6 2 83 mp2an 
 |-  ( ( C vH A ) MH B <-> A. x e. CH ( x C_ B -> ( ( x vH ( C vH A ) ) i^i B ) C_ ( x vH ( ( C vH A ) i^i B ) ) ) )
85 82 84 sylibr 
 |-  ( ( A MH B /\ C MH ( A vH B ) /\ ( C i^i ( A vH B ) ) C_ A ) -> ( C vH A ) MH B )
86 3 1 chjcomi 
 |-  ( C vH A ) = ( A vH C )
87 incom 
 |-  ( B i^i ( A vH B ) ) = ( ( A vH B ) i^i B )
88 18 87 19 3eqtr3ri 
 |-  B = ( ( A vH B ) i^i B )
89 86 88 ineq12i 
 |-  ( ( C vH A ) i^i B ) = ( ( A vH C ) i^i ( ( A vH B ) i^i B ) )
90 inass 
 |-  ( ( ( A vH C ) i^i ( A vH B ) ) i^i B ) = ( ( A vH C ) i^i ( ( A vH B ) i^i B ) )
91 1 2 chub1i 
 |-  A C_ ( A vH B )
92 mdi 
 |-  ( ( ( C e. CH /\ ( A vH B ) e. CH /\ A e. CH ) /\ ( C MH ( A vH B ) /\ A C_ ( A vH B ) ) ) -> ( ( A vH C ) i^i ( A vH B ) ) = ( A vH ( C i^i ( A vH B ) ) ) )
93 92 exp32 
 |-  ( ( C e. CH /\ ( A vH B ) e. CH /\ A e. CH ) -> ( C MH ( A vH B ) -> ( A C_ ( A vH B ) -> ( ( A vH C ) i^i ( A vH B ) ) = ( A vH ( C i^i ( A vH B ) ) ) ) ) )
94 3 29 1 93 mp3an 
 |-  ( C MH ( A vH B ) -> ( A C_ ( A vH B ) -> ( ( A vH C ) i^i ( A vH B ) ) = ( A vH ( C i^i ( A vH B ) ) ) ) )
95 91 94 mpi 
 |-  ( C MH ( A vH B ) -> ( ( A vH C ) i^i ( A vH B ) ) = ( A vH ( C i^i ( A vH B ) ) ) )
96 1 38 chjcomi 
 |-  ( A vH ( C i^i ( A vH B ) ) ) = ( ( C i^i ( A vH B ) ) vH A )
97 38 1 chlejb1i 
 |-  ( ( C i^i ( A vH B ) ) C_ A <-> ( ( C i^i ( A vH B ) ) vH A ) = A )
98 97 biimpi 
 |-  ( ( C i^i ( A vH B ) ) C_ A -> ( ( C i^i ( A vH B ) ) vH A ) = A )
99 96 98 syl5eq 
 |-  ( ( C i^i ( A vH B ) ) C_ A -> ( A vH ( C i^i ( A vH B ) ) ) = A )
100 95 99 sylan9eq 
 |-  ( ( C MH ( A vH B ) /\ ( C i^i ( A vH B ) ) C_ A ) -> ( ( A vH C ) i^i ( A vH B ) ) = A )
101 100 ineq1d 
 |-  ( ( C MH ( A vH B ) /\ ( C i^i ( A vH B ) ) C_ A ) -> ( ( ( A vH C ) i^i ( A vH B ) ) i^i B ) = ( A i^i B ) )
102 90 101 eqtr3id 
 |-  ( ( C MH ( A vH B ) /\ ( C i^i ( A vH B ) ) C_ A ) -> ( ( A vH C ) i^i ( ( A vH B ) i^i B ) ) = ( A i^i B ) )
103 89 102 syl5eq 
 |-  ( ( C MH ( A vH B ) /\ ( C i^i ( A vH B ) ) C_ A ) -> ( ( C vH A ) i^i B ) = ( A i^i B ) )
104 103 3adant1 
 |-  ( ( A MH B /\ C MH ( A vH B ) /\ ( C i^i ( A vH B ) ) C_ A ) -> ( ( C vH A ) i^i B ) = ( A i^i B ) )
105 85 104 jca 
 |-  ( ( A MH B /\ C MH ( A vH B ) /\ ( C i^i ( A vH B ) ) C_ A ) -> ( ( C vH A ) MH B /\ ( ( C vH A ) i^i B ) = ( A i^i B ) ) )