MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lmiisolem Structured version   Visualization version   Unicode version

Theorem lmiisolem 24838
Description: Lemma for lmiiso 24839. (Contributed by Thierry Arnoux, 14-Dec-2019.)
Hypotheses
Ref Expression
ismid.p  |-  P  =  ( Base `  G
)
ismid.d  |-  .-  =  ( dist `  G )
ismid.i  |-  I  =  (Itv `  G )
ismid.g  |-  ( ph  ->  G  e. TarskiG )
ismid.1  |-  ( ph  ->  GDimTarskiG 2 )
lmif.m  |-  M  =  ( (lInvG `  G
) `  D )
lmif.l  |-  L  =  (LineG `  G )
lmif.d  |-  ( ph  ->  D  e.  ran  L
)
lmiiso.1  |-  ( ph  ->  A  e.  P )
lmiiso.2  |-  ( ph  ->  B  e.  P )
lmiisolem.s  |-  S  =  ( (pInvG `  G
) `  Z )
lmiisolem.z  |-  Z  =  ( ( A (midG `  G ) ( M `
 A ) ) (midG `  G )
( B (midG `  G ) ( M `
 B ) ) )
Assertion
Ref Expression
lmiisolem  |-  ( ph  ->  ( ( M `  A )  .-  ( M `  B )
)  =  ( A 
.-  B ) )

Proof of Theorem lmiisolem
StepHypRef Expression
1 ismid.p . . . . . . . 8  |-  P  =  ( Base `  G
)
2 ismid.d . . . . . . . 8  |-  .-  =  ( dist `  G )
3 ismid.i . . . . . . . 8  |-  I  =  (Itv `  G )
4 ismid.g . . . . . . . . 9  |-  ( ph  ->  G  e. TarskiG )
54adantr 467 . . . . . . . 8  |-  ( (
ph  /\  ( S `  A )  =  Z )  ->  G  e. TarskiG )
6 lmiisolem.z . . . . . . . . . 10  |-  Z  =  ( ( A (midG `  G ) ( M `
 A ) ) (midG `  G )
( B (midG `  G ) ( M `
 B ) ) )
7 ismid.1 . . . . . . . . . . 11  |-  ( ph  ->  GDimTarskiG 2 )
8 lmiiso.1 . . . . . . . . . . . 12  |-  ( ph  ->  A  e.  P )
9 lmif.m . . . . . . . . . . . . 13  |-  M  =  ( (lInvG `  G
) `  D )
10 lmif.l . . . . . . . . . . . . 13  |-  L  =  (LineG `  G )
11 lmif.d . . . . . . . . . . . . 13  |-  ( ph  ->  D  e.  ran  L
)
121, 2, 3, 4, 7, 9, 10, 11, 8lmicl 24828 . . . . . . . . . . . 12  |-  ( ph  ->  ( M `  A
)  e.  P )
131, 2, 3, 4, 7, 8, 12midcl 24819 . . . . . . . . . . 11  |-  ( ph  ->  ( A (midG `  G ) ( M `
 A ) )  e.  P )
14 lmiiso.2 . . . . . . . . . . . 12  |-  ( ph  ->  B  e.  P )
151, 2, 3, 4, 7, 9, 10, 11, 14lmicl 24828 . . . . . . . . . . . 12  |-  ( ph  ->  ( M `  B
)  e.  P )
161, 2, 3, 4, 7, 14, 15midcl 24819 . . . . . . . . . . 11  |-  ( ph  ->  ( B (midG `  G ) ( M `
 B ) )  e.  P )
171, 2, 3, 4, 7, 13, 16midcl 24819 . . . . . . . . . 10  |-  ( ph  ->  ( ( A (midG `  G ) ( M `
 A ) ) (midG `  G )
( B (midG `  G ) ( M `
 B ) ) )  e.  P )
186, 17syl5eqel 2533 . . . . . . . . 9  |-  ( ph  ->  Z  e.  P )
1918adantr 467 . . . . . . . 8  |-  ( (
ph  /\  ( S `  A )  =  Z )  ->  Z  e.  P )
20 eqid 2451 . . . . . . . . . 10  |-  (pInvG `  G )  =  (pInvG `  G )
21 lmiisolem.s . . . . . . . . . 10  |-  S  =  ( (pInvG `  G
) `  Z )
221, 2, 3, 10, 20, 4, 18, 21, 8mircl 24706 . . . . . . . . 9  |-  ( ph  ->  ( S `  A
)  e.  P )
2322adantr 467 . . . . . . . 8  |-  ( (
ph  /\  ( S `  A )  =  Z )  ->  ( S `  A )  e.  P
)
248adantr 467 . . . . . . . 8  |-  ( (
ph  /\  ( S `  A )  =  Z )  ->  A  e.  P )
251, 2, 3, 10, 20, 5, 19, 21, 24mircgr 24702 . . . . . . . 8  |-  ( (
ph  /\  ( S `  A )  =  Z )  ->  ( Z  .-  ( S `  A
) )  =  ( Z  .-  A ) )
26 simpr 463 . . . . . . . . 9  |-  ( (
ph  /\  ( S `  A )  =  Z )  ->  ( S `  A )  =  Z )
2726eqcomd 2457 . . . . . . . 8  |-  ( (
ph  /\  ( S `  A )  =  Z )  ->  Z  =  ( S `  A ) )
281, 2, 3, 5, 19, 23, 19, 24, 25, 27tgcgreq 24526 . . . . . . 7  |-  ( (
ph  /\  ( S `  A )  =  Z )  ->  Z  =  A )
29 simpr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( A
(midG `  G )
( M `  A
) )  =  ( B (midG `  G
) ( M `  B ) ) )  ->  ( A (midG `  G ) ( M `
 A ) )  =  ( B (midG `  G ) ( M `
 B ) ) )
3029oveq2d 6306 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( A
(midG `  G )
( M `  A
) )  =  ( B (midG `  G
) ( M `  B ) ) )  ->  ( ( A (midG `  G )
( M `  A
) ) (midG `  G ) ( A (midG `  G )
( M `  A
) ) )  =  ( ( A (midG `  G ) ( M `
 A ) ) (midG `  G )
( B (midG `  G ) ( M `
 B ) ) ) )
3130, 6syl6reqr 2504 . . . . . . . . . . 11  |-  ( (
ph  /\  ( A
(midG `  G )
( M `  A
) )  =  ( B (midG `  G
) ( M `  B ) ) )  ->  Z  =  ( ( A (midG `  G ) ( M `
 A ) ) (midG `  G )
( A (midG `  G ) ( M `
 A ) ) ) )
324adantr 467 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( A
(midG `  G )
( M `  A
) )  =  ( B (midG `  G
) ( M `  B ) ) )  ->  G  e. TarskiG )
337adantr 467 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( A
(midG `  G )
( M `  A
) )  =  ( B (midG `  G
) ( M `  B ) ) )  ->  GDimTarskiG 2 )
3413adantr 467 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( A
(midG `  G )
( M `  A
) )  =  ( B (midG `  G
) ( M `  B ) ) )  ->  ( A (midG `  G ) ( M `
 A ) )  e.  P )
351, 2, 3, 32, 33, 34, 34midid 24823 . . . . . . . . . . 11  |-  ( (
ph  /\  ( A
(midG `  G )
( M `  A
) )  =  ( B (midG `  G
) ( M `  B ) ) )  ->  ( ( A (midG `  G )
( M `  A
) ) (midG `  G ) ( A (midG `  G )
( M `  A
) ) )  =  ( A (midG `  G ) ( M `
 A ) ) )
3631, 35eqtrd 2485 . . . . . . . . . 10  |-  ( (
ph  /\  ( A
(midG `  G )
( M `  A
) )  =  ( B (midG `  G
) ( M `  B ) ) )  ->  Z  =  ( A (midG `  G
) ( M `  A ) ) )
37 eqidd 2452 . . . . . . . . . . . . 13  |-  ( ph  ->  ( M `  A
)  =  ( M `
 A ) )
381, 2, 3, 4, 7, 9, 10, 11, 8, 12islmib 24829 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( M `  A )  =  ( M `  A )  <-> 
( ( A (midG `  G ) ( M `
 A ) )  e.  D  /\  ( D (⟂G `  G )
( A L ( M `  A ) )  \/  A  =  ( M `  A
) ) ) ) )
3937, 38mpbid 214 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( A (midG `  G ) ( M `
 A ) )  e.  D  /\  ( D (⟂G `  G )
( A L ( M `  A ) )  \/  A  =  ( M `  A
) ) ) )
4039simpld 461 . . . . . . . . . . 11  |-  ( ph  ->  ( A (midG `  G ) ( M `
 A ) )  e.  D )
4140adantr 467 . . . . . . . . . 10  |-  ( (
ph  /\  ( A
(midG `  G )
( M `  A
) )  =  ( B (midG `  G
) ( M `  B ) ) )  ->  ( A (midG `  G ) ( M `
 A ) )  e.  D )
4236, 41eqeltrd 2529 . . . . . . . . 9  |-  ( (
ph  /\  ( A
(midG `  G )
( M `  A
) )  =  ( B (midG `  G
) ( M `  B ) ) )  ->  Z  e.  D
)
434adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  ( A
(midG `  G )
( M `  A
) )  =/=  ( B (midG `  G )
( M `  B
) ) )  ->  G  e. TarskiG )
4413adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  ( A
(midG `  G )
( M `  A
) )  =/=  ( B (midG `  G )
( M `  B
) ) )  -> 
( A (midG `  G ) ( M `
 A ) )  e.  P )
4516adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  ( A
(midG `  G )
( M `  A
) )  =/=  ( B (midG `  G )
( M `  B
) ) )  -> 
( B (midG `  G ) ( M `
 B ) )  e.  P )
4618adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  ( A
(midG `  G )
( M `  A
) )  =/=  ( B (midG `  G )
( M `  B
) ) )  ->  Z  e.  P )
47 simpr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  ( A
(midG `  G )
( M `  A
) )  =/=  ( B (midG `  G )
( M `  B
) ) )  -> 
( A (midG `  G ) ( M `
 A ) )  =/=  ( B (midG `  G ) ( M `
 B ) ) )
481, 2, 3, 4, 7, 13, 16midbtwn 24821 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( A (midG `  G ) ( M `
 A ) ) (midG `  G )
( B (midG `  G ) ( M `
 B ) ) )  e.  ( ( A (midG `  G
) ( M `  A ) ) I ( B (midG `  G ) ( M `
 B ) ) ) )
496, 48syl5eqel 2533 . . . . . . . . . . . 12  |-  ( ph  ->  Z  e.  ( ( A (midG `  G
) ( M `  A ) ) I ( B (midG `  G ) ( M `
 B ) ) ) )
5049adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  ( A
(midG `  G )
( M `  A
) )  =/=  ( B (midG `  G )
( M `  B
) ) )  ->  Z  e.  ( ( A (midG `  G )
( M `  A
) ) I ( B (midG `  G
) ( M `  B ) ) ) )
511, 3, 10, 43, 44, 45, 46, 47, 50btwnlng1 24664 . . . . . . . . . 10  |-  ( (
ph  /\  ( A
(midG `  G )
( M `  A
) )  =/=  ( B (midG `  G )
( M `  B
) ) )  ->  Z  e.  ( ( A (midG `  G )
( M `  A
) ) L ( B (midG `  G
) ( M `  B ) ) ) )
5211adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  ( A
(midG `  G )
( M `  A
) )  =/=  ( B (midG `  G )
( M `  B
) ) )  ->  D  e.  ran  L )
5340adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  ( A
(midG `  G )
( M `  A
) )  =/=  ( B (midG `  G )
( M `  B
) ) )  -> 
( A (midG `  G ) ( M `
 A ) )  e.  D )
54 eqidd 2452 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( M `  B
)  =  ( M `
 B ) )
551, 2, 3, 4, 7, 9, 10, 11, 14, 15islmib 24829 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( M `  B )  =  ( M `  B )  <-> 
( ( B (midG `  G ) ( M `
 B ) )  e.  D  /\  ( D (⟂G `  G )
( B L ( M `  B ) )  \/  B  =  ( M `  B
) ) ) ) )
5654, 55mpbid 214 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( B (midG `  G ) ( M `
 B ) )  e.  D  /\  ( D (⟂G `  G )
( B L ( M `  B ) )  \/  B  =  ( M `  B
) ) ) )
5756simpld 461 . . . . . . . . . . . 12  |-  ( ph  ->  ( B (midG `  G ) ( M `
 B ) )  e.  D )
5857adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  ( A
(midG `  G )
( M `  A
) )  =/=  ( B (midG `  G )
( M `  B
) ) )  -> 
( B (midG `  G ) ( M `
 B ) )  e.  D )
591, 3, 10, 43, 44, 45, 47, 47, 52, 53, 58tglinethru 24681 . . . . . . . . . 10  |-  ( (
ph  /\  ( A
(midG `  G )
( M `  A
) )  =/=  ( B (midG `  G )
( M `  B
) ) )  ->  D  =  ( ( A (midG `  G )
( M `  A
) ) L ( B (midG `  G
) ( M `  B ) ) ) )
6051, 59eleqtrrd 2532 . . . . . . . . 9  |-  ( (
ph  /\  ( A
(midG `  G )
( M `  A
) )  =/=  ( B (midG `  G )
( M `  B
) ) )  ->  Z  e.  D )
6142, 60pm2.61dane 2711 . . . . . . . 8  |-  ( ph  ->  Z  e.  D )
6261adantr 467 . . . . . . 7  |-  ( (
ph  /\  ( S `  A )  =  Z )  ->  Z  e.  D )
6328, 62eqeltrrd 2530 . . . . . 6  |-  ( (
ph  /\  ( S `  A )  =  Z )  ->  A  e.  D )
641, 2, 3, 4, 7, 9, 10, 11, 8lmiinv 24834 . . . . . . 7  |-  ( ph  ->  ( ( M `  A )  =  A  <-> 
A  e.  D ) )
6564biimpar 488 . . . . . 6  |-  ( (
ph  /\  A  e.  D )  ->  ( M `  A )  =  A )
6663, 65syldan 473 . . . . 5  |-  ( (
ph  /\  ( S `  A )  =  Z )  ->  ( M `  A )  =  A )
6766, 28eqtr4d 2488 . . . 4  |-  ( (
ph  /\  ( S `  A )  =  Z )  ->  ( M `  A )  =  Z )
6867oveq1d 6305 . . 3  |-  ( (
ph  /\  ( S `  A )  =  Z )  ->  ( ( M `  A )  .-  ( M `  B
) )  =  ( Z  .-  ( M `
 B ) ) )
69 eqidd 2452 . . . . . . . . 9  |-  ( (
ph  /\  B  =  ( M `  B ) )  ->  Z  =  Z )
704adantr 467 . . . . . . . . . 10  |-  ( (
ph  /\  B  =  ( M `  B ) )  ->  G  e. TarskiG )
7114adantr 467 . . . . . . . . . 10  |-  ( (
ph  /\  B  =  ( M `  B ) )  ->  B  e.  P )
7216adantr 467 . . . . . . . . . 10  |-  ( (
ph  /\  B  =  ( M `  B ) )  ->  ( B
(midG `  G )
( M `  B
) )  e.  P
)
731, 2, 3, 4, 7, 14, 15midbtwn 24821 . . . . . . . . . . . 12  |-  ( ph  ->  ( B (midG `  G ) ( M `
 B ) )  e.  ( B I ( M `  B
) ) )
7473adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  B  =  ( M `  B ) )  ->  ( B
(midG `  G )
( M `  B
) )  e.  ( B I ( M `
 B ) ) )
75 simpr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  B  =  ( M `  B ) )  ->  B  =  ( M `  B ) )
7675oveq2d 6306 . . . . . . . . . . 11  |-  ( (
ph  /\  B  =  ( M `  B ) )  ->  ( B I B )  =  ( B I ( M `
 B ) ) )
7774, 76eleqtrrd 2532 . . . . . . . . . 10  |-  ( (
ph  /\  B  =  ( M `  B ) )  ->  ( B
(midG `  G )
( M `  B
) )  e.  ( B I B ) )
781, 2, 3, 70, 71, 72, 77axtgbtwnid 24514 . . . . . . . . 9  |-  ( (
ph  /\  B  =  ( M `  B ) )  ->  B  =  ( B (midG `  G
) ( M `  B ) ) )
79 eqidd 2452 . . . . . . . . 9  |-  ( (
ph  /\  B  =  ( M `  B ) )  ->  B  =  B )
8069, 78, 79s3eqd 12959 . . . . . . . 8  |-  ( (
ph  /\  B  =  ( M `  B ) )  ->  <" Z B B ">  =  <" Z ( B (midG `  G )
( M `  B
) ) B "> )
811, 2, 3, 10, 20, 4, 18, 14, 14ragtrivb 24747 . . . . . . . . 9  |-  ( ph  ->  <" Z B B ">  e.  (∟G `  G ) )
8281adantr 467 . . . . . . . 8  |-  ( (
ph  /\  B  =  ( M `  B ) )  ->  <" Z B B ">  e.  (∟G `  G ) )
8380, 82eqeltrrd 2530 . . . . . . 7  |-  ( (
ph  /\  B  =  ( M `  B ) )  ->  <" Z
( B (midG `  G ) ( M `
 B ) ) B ">  e.  (∟G `  G ) )
844adantr 467 . . . . . . . 8  |-  ( (
ph  /\  B  =/=  ( M `  B ) )  ->  G  e. TarskiG )
8561adantr 467 . . . . . . . 8  |-  ( (
ph  /\  B  =/=  ( M `  B ) )  ->  Z  e.  D )
8657adantr 467 . . . . . . . 8  |-  ( (
ph  /\  B  =/=  ( M `  B ) )  ->  ( B
(midG `  G )
( M `  B
) )  e.  D
)
8714adantr 467 . . . . . . . 8  |-  ( (
ph  /\  B  =/=  ( M `  B ) )  ->  B  e.  P )
88 df-ne 2624 . . . . . . . . . 10  |-  ( B  =/=  ( M `  B )  <->  -.  B  =  ( M `  B ) )
8956simprd 465 . . . . . . . . . . . 12  |-  ( ph  ->  ( D (⟂G `  G
) ( B L ( M `  B
) )  \/  B  =  ( M `  B ) ) )
9089orcomd 390 . . . . . . . . . . 11  |-  ( ph  ->  ( B  =  ( M `  B )  \/  D (⟂G `  G
) ( B L ( M `  B
) ) ) )
9190orcanai 924 . . . . . . . . . 10  |-  ( (
ph  /\  -.  B  =  ( M `  B ) )  ->  D (⟂G `  G )
( B L ( M `  B ) ) )
9288, 91sylan2b 478 . . . . . . . . 9  |-  ( (
ph  /\  B  =/=  ( M `  B ) )  ->  D (⟂G `  G ) ( B L ( M `  B ) ) )
9315adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  B  =/=  ( M `  B ) )  ->  ( M `  B )  e.  P
)
94 simpr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  B  =/=  ( M `  B ) )  ->  B  =/=  ( M `  B ) )
9516adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  B  =/=  ( M `  B ) )  ->  ( B
(midG `  G )
( M `  B
) )  e.  P
)
964adantr 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B
(midG `  G )
( M `  B
) )  =  B )  ->  G  e. TarskiG )
9714adantr 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B
(midG `  G )
( M `  B
) )  =  B )  ->  B  e.  P )
9815adantr 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B
(midG `  G )
( M `  B
) )  =  B )  ->  ( M `  B )  e.  P
)
997adantr 467 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( B
(midG `  G )
( M `  B
) )  =  B )  ->  GDimTarskiG 2 )
100 simpr 463 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( B
(midG `  G )
( M `  B
) )  =  B )  ->  ( B
(midG `  G )
( M `  B
) )  =  B )
1011, 2, 3, 96, 99, 97, 98, 100midcgr 24822 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B
(midG `  G )
( M `  B
) )  =  B )  ->  ( B  .-  B )  =  ( B  .-  ( M `
 B ) ) )
102101eqcomd 2457 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B
(midG `  G )
( M `  B
) )  =  B )  ->  ( B  .-  ( M `  B
) )  =  ( B  .-  B ) )
1031, 2, 3, 96, 97, 98, 97, 102axtgcgrid 24511 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( B
(midG `  G )
( M `  B
) )  =  B )  ->  B  =  ( M `  B ) )
104103ex 436 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( B (midG `  G ) ( M `
 B ) )  =  B  ->  B  =  ( M `  B ) ) )
105104necon3d 2645 . . . . . . . . . . . 12  |-  ( ph  ->  ( B  =/=  ( M `  B )  ->  ( B (midG `  G ) ( M `
 B ) )  =/=  B ) )
106105imp 431 . . . . . . . . . . 11  |-  ( (
ph  /\  B  =/=  ( M `  B ) )  ->  ( B
(midG `  G )
( M `  B
) )  =/=  B
)
10773adantr 467 . . . . . . . . . . . 12  |-  ( (
ph  /\  B  =/=  ( M `  B ) )  ->  ( B
(midG `  G )
( M `  B
) )  e.  ( B I ( M `
 B ) ) )
1081, 3, 10, 84, 87, 93, 95, 94, 107btwnlng1 24664 . . . . . . . . . . 11  |-  ( (
ph  /\  B  =/=  ( M `  B ) )  ->  ( B
(midG `  G )
( M `  B
) )  e.  ( B L ( M `
 B ) ) )
1091, 3, 10, 84, 87, 93, 94, 95, 106, 108tglineelsb2 24677 . . . . . . . . . 10  |-  ( (
ph  /\  B  =/=  ( M `  B ) )  ->  ( B L ( M `  B ) )  =  ( B L ( B (midG `  G
) ( M `  B ) ) ) )
1101, 3, 10, 84, 95, 87, 106tglinecom 24680 . . . . . . . . . 10  |-  ( (
ph  /\  B  =/=  ( M `  B ) )  ->  ( ( B (midG `  G )
( M `  B
) ) L B )  =  ( B L ( B (midG `  G ) ( M `
 B ) ) ) )
111109, 110eqtr4d 2488 . . . . . . . . 9  |-  ( (
ph  /\  B  =/=  ( M `  B ) )  ->  ( B L ( M `  B ) )  =  ( ( B (midG `  G ) ( M `
 B ) ) L B ) )
11292, 111breqtrd 4427 . . . . . . . 8  |-  ( (
ph  /\  B  =/=  ( M `  B ) )  ->  D (⟂G `  G ) ( ( B (midG `  G
) ( M `  B ) ) L B ) )
1131, 2, 3, 10, 84, 85, 86, 87, 112perpdrag 24770 . . . . . . 7  |-  ( (
ph  /\  B  =/=  ( M `  B ) )  ->  <" Z
( B (midG `  G ) ( M `
 B ) ) B ">  e.  (∟G `  G ) )
11483, 113pm2.61dane 2711 . . . . . 6  |-  ( ph  ->  <" Z ( B (midG `  G
) ( M `  B ) ) B ">  e.  (∟G `  G ) )
1151, 2, 3, 10, 20, 4, 18, 16, 14israg 24742 . . . . . 6  |-  ( ph  ->  ( <" Z
( B (midG `  G ) ( M `
 B ) ) B ">  e.  (∟G `  G )  <->  ( Z  .-  B )  =  ( Z  .-  ( ( (pInvG `  G ) `  ( B (midG `  G ) ( M `
 B ) ) ) `  B ) ) ) )
116114, 115mpbid 214 . . . . 5  |-  ( ph  ->  ( Z  .-  B
)  =  ( Z 
.-  ( ( (pInvG `  G ) `  ( B (midG `  G )
( M `  B
) ) ) `  B ) ) )
117 eqidd 2452 . . . . . . 7  |-  ( ph  ->  ( B (midG `  G ) ( M `
 B ) )  =  ( B (midG `  G ) ( M `
 B ) ) )
1181, 2, 3, 4, 7, 14, 15, 20, 16ismidb 24820 . . . . . . 7  |-  ( ph  ->  ( ( M `  B )  =  ( ( (pInvG `  G
) `  ( B
(midG `  G )
( M `  B
) ) ) `  B )  <->  ( B
(midG `  G )
( M `  B
) )  =  ( B (midG `  G
) ( M `  B ) ) ) )
119117, 118mpbird 236 . . . . . 6  |-  ( ph  ->  ( M `  B
)  =  ( ( (pInvG `  G ) `  ( B (midG `  G ) ( M `
 B ) ) ) `  B ) )
120119oveq2d 6306 . . . . 5  |-  ( ph  ->  ( Z  .-  ( M `  B )
)  =  ( Z 
.-  ( ( (pInvG `  G ) `  ( B (midG `  G )
( M `  B
) ) ) `  B ) ) )
121116, 120eqtr4d 2488 . . . 4  |-  ( ph  ->  ( Z  .-  B
)  =  ( Z 
.-  ( M `  B ) ) )
122121adantr 467 . . 3  |-  ( (
ph  /\  ( S `  A )  =  Z )  ->  ( Z  .-  B )  =  ( Z  .-  ( M `
 B ) ) )
12328oveq1d 6305 . . 3  |-  ( (
ph  /\  ( S `  A )  =  Z )  ->  ( Z  .-  B )  =  ( A  .-  B ) )
12468, 122, 1233eqtr2d 2491 . 2  |-  ( (
ph  /\  ( S `  A )  =  Z )  ->  ( ( M `  A )  .-  ( M `  B
) )  =  ( A  .-  B ) )
1254adantr 467 . . . 4  |-  ( (
ph  /\  ( S `  A )  =/=  Z
)  ->  G  e. TarskiG )
12622adantr 467 . . . 4  |-  ( (
ph  /\  ( S `  A )  =/=  Z
)  ->  ( S `  A )  e.  P
)
12718adantr 467 . . . 4  |-  ( (
ph  /\  ( S `  A )  =/=  Z
)  ->  Z  e.  P )
1288adantr 467 . . . 4  |-  ( (
ph  /\  ( S `  A )  =/=  Z
)  ->  A  e.  P )
1291, 2, 3, 10, 20, 4, 18, 21, 12mircl 24706 . . . . 5  |-  ( ph  ->  ( S `  ( M `  A )
)  e.  P )
130129adantr 467 . . . 4  |-  ( (
ph  /\  ( S `  A )  =/=  Z
)  ->  ( S `  ( M `  A
) )  e.  P
)
13112adantr 467 . . . 4  |-  ( (
ph  /\  ( S `  A )  =/=  Z
)  ->  ( M `  A )  e.  P
)
13214adantr 467 . . . 4  |-  ( (
ph  /\  ( S `  A )  =/=  Z
)  ->  B  e.  P )
13315adantr 467 . . . 4  |-  ( (
ph  /\  ( S `  A )  =/=  Z
)  ->  ( M `  B )  e.  P
)
134 simpr 463 . . . 4  |-  ( (
ph  /\  ( S `  A )  =/=  Z
)  ->  ( S `  A )  =/=  Z
)
1351, 2, 3, 10, 20, 125, 127, 21, 128mirbtwn 24703 . . . 4  |-  ( (
ph  /\  ( S `  A )  =/=  Z
)  ->  Z  e.  ( ( S `  A ) I A ) )
1361, 2, 3, 10, 20, 125, 127, 21, 131mirbtwn 24703 . . . 4  |-  ( (
ph  /\  ( S `  A )  =/=  Z
)  ->  Z  e.  ( ( S `  ( M `  A ) ) I ( M `
 A ) ) )
137 eqidd 2452 . . . . . . . . . . . 12  |-  ( (
ph  /\  A  =  ( M `  A ) )  ->  Z  =  Z )
1384adantr 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  A  =  ( M `  A ) )  ->  G  e. TarskiG )
1398adantr 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  A  =  ( M `  A ) )  ->  A  e.  P )
14013adantr 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  A  =  ( M `  A ) )  ->  ( A
(midG `  G )
( M `  A
) )  e.  P
)
1411, 2, 3, 4, 7, 8, 12midbtwn 24821 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( A (midG `  G ) ( M `
 A ) )  e.  ( A I ( M `  A
) ) )
142141adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  A  =  ( M `  A ) )  ->  ( A
(midG `  G )
( M `  A
) )  e.  ( A I ( M `
 A ) ) )
143 simpr 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  A  =  ( M `  A ) )  ->  A  =  ( M `  A ) )
144143oveq2d 6306 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  A  =  ( M `  A ) )  ->  ( A I A )  =  ( A I ( M `
 A ) ) )
145142, 144eleqtrrd 2532 . . . . . . . . . . . . 13  |-  ( (
ph  /\  A  =  ( M `  A ) )  ->  ( A
(midG `  G )
( M `  A
) )  e.  ( A I A ) )
1461, 2, 3, 138, 139, 140, 145axtgbtwnid 24514 . . . . . . . . . . . 12  |-  ( (
ph  /\  A  =  ( M `  A ) )  ->  A  =  ( A (midG `  G
) ( M `  A ) ) )
147 eqidd 2452 . . . . . . . . . . . 12  |-  ( (
ph  /\  A  =  ( M `  A ) )  ->  A  =  A )
148137, 146, 147s3eqd 12959 . . . . . . . . . . 11  |-  ( (
ph  /\  A  =  ( M `  A ) )  ->  <" Z A A ">  =  <" Z ( A (midG `  G )
( M `  A
) ) A "> )
1491, 2, 3, 10, 20, 4, 18, 8, 8ragtrivb 24747 . . . . . . . . . . . 12  |-  ( ph  ->  <" Z A A ">  e.  (∟G `  G ) )
150149adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  A  =  ( M `  A ) )  ->  <" Z A A ">  e.  (∟G `  G ) )
151148, 150eqeltrrd 2530 . . . . . . . . . 10  |-  ( (
ph  /\  A  =  ( M `  A ) )  ->  <" Z
( A (midG `  G ) ( M `
 A ) ) A ">  e.  (∟G `  G ) )
1524adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  A  =/=  ( M `  A ) )  ->  G  e. TarskiG )
15361adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  A  =/=  ( M `  A ) )  ->  Z  e.  D )
15440adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  A  =/=  ( M `  A ) )  ->  ( A
(midG `  G )
( M `  A
) )  e.  D
)
1558adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  A  =/=  ( M `  A ) )  ->  A  e.  P )
156 df-ne 2624 . . . . . . . . . . . . 13  |-  ( A  =/=  ( M `  A )  <->  -.  A  =  ( M `  A ) )
15739simprd 465 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( D (⟂G `  G
) ( A L ( M `  A
) )  \/  A  =  ( M `  A ) ) )
158157orcomd 390 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A  =  ( M `  A )  \/  D (⟂G `  G
) ( A L ( M `  A
) ) ) )
159158orcanai 924 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  A  =  ( M `  A ) )  ->  D (⟂G `  G )
( A L ( M `  A ) ) )
160156, 159sylan2b 478 . . . . . . . . . . . 12  |-  ( (
ph  /\  A  =/=  ( M `  A ) )  ->  D (⟂G `  G ) ( A L ( M `  A ) ) )
16112adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  A  =/=  ( M `  A ) )  ->  ( M `  A )  e.  P
)
162 simpr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  A  =/=  ( M `  A ) )  ->  A  =/=  ( M `  A ) )
16313adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  A  =/=  ( M `  A ) )  ->  ( A
(midG `  G )
( M `  A
) )  e.  P
)
1644adantr 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( A
(midG `  G )
( M `  A
) )  =  A )  ->  G  e. TarskiG )
1658adantr 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( A
(midG `  G )
( M `  A
) )  =  A )  ->  A  e.  P )
16612adantr 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( A
(midG `  G )
( M `  A
) )  =  A )  ->  ( M `  A )  e.  P
)
1677adantr 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( A
(midG `  G )
( M `  A
) )  =  A )  ->  GDimTarskiG 2 )
168 simpr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( A
(midG `  G )
( M `  A
) )  =  A )  ->  ( A
(midG `  G )
( M `  A
) )  =  A )
1691, 2, 3, 164, 167, 165, 166, 168midcgr 24822 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( A
(midG `  G )
( M `  A
) )  =  A )  ->  ( A  .-  A )  =  ( A  .-  ( M `
 A ) ) )
170169eqcomd 2457 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( A
(midG `  G )
( M `  A
) )  =  A )  ->  ( A  .-  ( M `  A
) )  =  ( A  .-  A ) )
1711, 2, 3, 164, 165, 166, 165, 170axtgcgrid 24511 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( A
(midG `  G )
( M `  A
) )  =  A )  ->  A  =  ( M `  A ) )
172171ex 436 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( A (midG `  G ) ( M `
 A ) )  =  A  ->  A  =  ( M `  A ) ) )
173172necon3d 2645 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( A  =/=  ( M `  A )  ->  ( A (midG `  G ) ( M `
 A ) )  =/=  A ) )
174173imp 431 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  A  =/=  ( M `  A ) )  ->  ( A
(midG `  G )
( M `  A
) )  =/=  A
)
175141adantr 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  A  =/=  ( M `  A ) )  ->  ( A
(midG `  G )
( M `  A
) )  e.  ( A I ( M `
 A ) ) )
1761, 3, 10, 152, 155, 161, 163, 162, 175btwnlng1 24664 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  A  =/=  ( M `  A ) )  ->  ( A
(midG `  G )
( M `  A
) )  e.  ( A L ( M `
 A ) ) )
1771, 3, 10, 152, 155, 161, 162, 163, 174, 176tglineelsb2 24677 . . . . . . . . . . . . 13  |-  ( (
ph  /\  A  =/=  ( M `  A ) )  ->  ( A L ( M `  A ) )  =  ( A L ( A (midG `  G
) ( M `  A ) ) ) )
1781, 3, 10, 152, 163, 155, 174tglinecom 24680 . . . . . . . . . . . . 13  |-  ( (
ph  /\  A  =/=  ( M `  A ) )  ->  ( ( A (midG `  G )
( M `  A
) ) L A )  =  ( A L ( A (midG `  G ) ( M `
 A ) ) ) )
179177, 178eqtr4d 2488 . . . . . . . . . . . 12  |-  ( (
ph  /\  A  =/=  ( M `  A ) )  ->  ( A L ( M `  A ) )  =  ( ( A (midG `  G ) ( M `
 A ) ) L A ) )
180160, 179breqtrd 4427 . . . . . . . . . . 11  |-  ( (
ph  /\  A  =/=  ( M `  A ) )  ->  D (⟂G `  G ) ( ( A (midG `  G
) ( M `  A ) ) L A ) )
1811, 2, 3, 10, 152, 153, 154, 155, 180perpdrag 24770 . . . . . . . . . 10  |-  ( (
ph  /\  A  =/=  ( M `  A ) )  ->  <" Z
( A (midG `  G ) ( M `
 A ) ) A ">  e.  (∟G `  G ) )
182151, 181pm2.61dane 2711 . . . . . . . . 9  |-  ( ph  ->  <" Z ( A (midG `  G
) ( M `  A ) ) A ">  e.  (∟G `  G ) )
1831, 2, 3, 10, 20, 4, 18, 13, 8israg 24742 . . . . . . . . 9  |-  ( ph  ->  ( <" Z
( A (midG `  G ) ( M `
 A ) ) A ">  e.  (∟G `  G )  <->  ( Z  .-  A )  =  ( Z  .-  ( ( (pInvG `  G ) `  ( A (midG `  G ) ( M `
 A ) ) ) `  A ) ) ) )
184182, 183mpbid 214 . . . . . . . 8  |-  ( ph  ->  ( Z  .-  A
)  =  ( Z 
.-  ( ( (pInvG `  G ) `  ( A (midG `  G )
( M `  A
) ) ) `  A ) ) )
185 eqidd 2452 . . . . . . . . . 10  |-  ( ph  ->  ( A (midG `  G ) ( M `
 A ) )  =  ( A (midG `  G ) ( M `
 A ) ) )
1861, 2, 3, 4, 7, 8, 12, 20, 13ismidb 24820 . . . . . . . . . 10  |-  ( ph  ->  ( ( M `  A )  =  ( ( (pInvG `  G
) `  ( A
(midG `  G )
( M `  A
) ) ) `  A )  <->  ( A
(midG `  G )
( M `  A
) )  =  ( A (midG `  G
) ( M `  A ) ) ) )
187185, 186mpbird 236 . . . . . . . . 9  |-  ( ph  ->  ( M `  A
)  =  ( ( (pInvG `  G ) `  ( A (midG `  G ) ( M `
 A ) ) ) `  A ) )
188187oveq2d 6306 . . . . . . . 8  |-  ( ph  ->  ( Z  .-  ( M `  A )
)  =  ( Z 
.-  ( ( (pInvG `  G ) `  ( A (midG `  G )
( M `  A
) ) ) `  A ) ) )
189184, 188eqtr4d 2488 . . . . . . 7  |-  ( ph  ->  ( Z  .-  A
)  =  ( Z 
.-  ( M `  A ) ) )
1901, 2, 3, 10, 20, 4, 18, 21, 8mircgr 24702 . . . . . . 7  |-  ( ph  ->  ( Z  .-  ( S `  A )
)  =  ( Z 
.-  A ) )
1911, 2, 3, 10, 20, 4, 18, 21, 12mircgr 24702 . . . . . . 7  |-  ( ph  ->  ( Z  .-  ( S `  ( M `  A ) ) )  =  ( Z  .-  ( M `  A ) ) )
192189, 190, 1913eqtr4d 2495 . . . . . 6  |-  ( ph  ->  ( Z  .-  ( S `  A )
)  =  ( Z 
.-  ( S `  ( M `  A ) ) ) )
193192adantr 467 . . . . 5  |-  ( (
ph  /\  ( S `  A )  =/=  Z
)  ->  ( Z  .-  ( S `  A
) )  =  ( Z  .-  ( S `
 ( M `  A ) ) ) )
1941, 2, 3, 125, 127, 126, 127, 130, 193tgcgrcomlr 24524 . . . 4  |-  ( (
ph  /\  ( S `  A )  =/=  Z
)  ->  ( ( S `  A )  .-  Z )  =  ( ( S `  ( M `  A )
)  .-  Z )
)
195189adantr 467 . . . 4  |-  ( (
ph  /\  ( S `  A )  =/=  Z
)  ->  ( Z  .-  A )  =  ( Z  .-  ( M `
 A ) ) )
19621fveq1i 5866 . . . . . . . . . 10  |-  ( S `
 ( A (midG `  G ) ( M `
 A ) ) )  =  ( ( (pInvG `  G ) `  Z ) `  ( A (midG `  G )
( M `  A
) ) )
1971, 2, 3, 4, 7, 8, 12, 21, 18mirmid 24825 . . . . . . . . . 10  |-  ( ph  ->  ( ( S `  A ) (midG `  G ) ( S `
 ( M `  A ) ) )  =  ( S `  ( A (midG `  G
) ( M `  A ) ) ) )
1986eqcomi 2460 . . . . . . . . . . 11  |-  ( ( A (midG `  G
) ( M `  A ) ) (midG `  G ) ( B (midG `  G )
( M `  B
) ) )  =  Z
1991, 2, 3, 4, 7, 13, 16, 20, 18ismidb 24820 . . . . . . . . . . 11  |-  ( ph  ->  ( ( B (midG `  G ) ( M `
 B ) )  =  ( ( (pInvG `  G ) `  Z
) `  ( A
(midG `  G )
( M `  A
) ) )  <->  ( ( A (midG `  G )
( M `  A
) ) (midG `  G ) ( B (midG `  G )
( M `  B
) ) )  =  Z ) )
200198, 199mpbiri 237 . . . . . . . . . 10  |-  ( ph  ->  ( B (midG `  G ) ( M `
 B ) )  =  ( ( (pInvG `  G ) `  Z
) `  ( A
(midG `  G )
( M `  A
) ) ) )
201196, 197, 2003eqtr4a 2511 . . . . . . . . 9  |-  ( ph  ->  ( ( S `  A ) (midG `  G ) ( S `
 ( M `  A ) ) )  =  ( B (midG `  G ) ( M `
 B ) ) )
2021, 2, 3, 4, 7, 22, 129, 20, 16ismidb 24820 . . . . . . . . 9  |-  ( ph  ->  ( ( S `  ( M `  A ) )  =  ( ( (pInvG `  G ) `  ( B (midG `  G ) ( M `
 B ) ) ) `  ( S `
 A ) )  <-> 
( ( S `  A ) (midG `  G ) ( S `
 ( M `  A ) ) )  =  ( B (midG `  G ) ( M `
 B ) ) ) )
203201, 202mpbird 236 . . . . . . . 8  |-  ( ph  ->  ( S `  ( M `  A )
)  =  ( ( (pInvG `  G ) `  ( B (midG `  G ) ( M `
 B ) ) ) `  ( S `
 A ) ) )
204119, 203oveq12d 6308 . . . . . . 7  |-  ( ph  ->  ( ( M `  B )  .-  ( S `  ( M `  A ) ) )  =  ( ( ( (pInvG `  G ) `  ( B (midG `  G ) ( M `
 B ) ) ) `  B ) 
.-  ( ( (pInvG `  G ) `  ( B (midG `  G )
( M `  B
) ) ) `  ( S `  A ) ) ) )
205 eqid 2451 . . . . . . . 8  |-  ( (pInvG `  G ) `  ( B (midG `  G )
( M `  B
) ) )  =  ( (pInvG `  G
) `  ( B
(midG `  G )
( M `  B
) ) )
2061, 2, 3, 10, 20, 4, 16, 205, 14, 22miriso 24715 . . . . . . 7  |-  ( ph  ->  ( ( ( (pInvG `  G ) `  ( B (midG `  G )
( M `  B
) ) ) `  B )  .-  (
( (pInvG `  G
) `  ( B
(midG `  G )
( M `  B
) ) ) `  ( S `  A ) ) )  =  ( B  .-  ( S `
 A ) ) )
207204, 206eqtr2d 2486 . . . . . 6  |-  ( ph  ->  ( B  .-  ( S `  A )
)  =  ( ( M `  B ) 
.-  ( S `  ( M `  A ) ) ) )
208207adantr 467 . . . . 5  |-  ( (
ph  /\  ( S `  A )  =/=  Z
)  ->  ( B  .-  ( S `  A
) )  =  ( ( M `  B
)  .-  ( S `  ( M `  A
) ) ) )
2091, 2, 3, 125, 132, 126, 133, 130, 208tgcgrcomlr 24524 . . . 4  |-  ( (
ph  /\  ( S `  A )  =/=  Z
)  ->  ( ( S `  A )  .-  B )  =  ( ( S `  ( M `  A )
)  .-  ( M `  B ) ) )
210121adantr 467 . . . 4  |-  ( (
ph  /\  ( S `  A )  =/=  Z
)  ->  ( Z  .-  B )  =  ( Z  .-  ( M `
 B ) ) )
2111, 2, 3, 125, 126, 127, 128, 130, 127, 131, 132, 133, 134, 135, 136, 194, 195, 209, 210axtg5seg 24513 . . 3  |-  ( (
ph  /\  ( S `  A )  =/=  Z
)  ->  ( A  .-  B )  =  ( ( M `  A
)  .-  ( M `  B ) ) )
212211eqcomd 2457 . 2  |-  ( (
ph  /\  ( S `  A )  =/=  Z
)  ->  ( ( M `  A )  .-  ( M `  B
) )  =  ( A  .-  B ) )
213124, 212pm2.61dane 2711 1  |-  ( ph  ->  ( ( M `  A )  .-  ( M `  B )
)  =  ( A 
.-  B ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 370    /\ wa 371    = wceq 1444    e. wcel 1887    =/= wne 2622   class class class wbr 4402   ran crn 4835   ` cfv 5582  (class class class)co 6290   2c2 10659   <"cs3 12938   Basecbs 15121   distcds 15199  TarskiGcstrkg 24478  DimTarskiGcstrkgld 24482  Itvcitv 24484  LineGclng 24485  pInvGcmir 24697  ∟Gcrag 24738  ⟂Gcperpg 24740  midGcmid 24814  lInvGclmi 24815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-rep 4515  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-reu 2744  df-rmo 2745  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-int 4235  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-tr 4498  df-eprel 4745  df-id 4749  df-po 4755  df-so 4756  df-fr 4793  df-we 4795  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-pred 5380  df-ord 5426  df-on 5427  df-lim 5428  df-suc 5429  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-riota 6252  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-om 6693  df-1st 6793  df-2nd 6794  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-1o 7182  df-oadd 7186  df-er 7363  df-map 7474  df-pm 7475  df-en 7570  df-dom 7571  df-sdom 7572  df-fin 7573  df-card 8373  df-cda 8598  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-nn 10610  df-2 10668  df-3 10669  df-n0 10870  df-z 10938  df-uz 11160  df-fz 11785  df-fzo 11916  df-hash 12516  df-word 12664  df-concat 12666  df-s1 12667  df-s2 12944  df-s3 12945  df-trkgc 24496  df-trkgb 24497  df-trkgcb 24498  df-trkgld 24500  df-trkg 24501  df-cgrg 24556  df-leg 24628  df-mir 24698  df-rag 24739  df-perpg 24741  df-mid 24816  df-lmi 24817
This theorem is referenced by:  lmiiso  24839
  Copyright terms: Public domain W3C validator