Metamath Proof Explorer


Theorem isinftm

Description: Express x is infinitesimal with respect to y for a structure W . (Contributed by Thierry Arnoux, 30-Jan-2018)

Ref Expression
Hypotheses inftm.b B = Base W
inftm.0 0 ˙ = 0 W
inftm.x · ˙ = W
inftm.l < ˙ = < W
Assertion isinftm W V X B Y B X W Y 0 ˙ < ˙ X n n · ˙ X < ˙ Y

Proof

Step Hyp Ref Expression
1 inftm.b B = Base W
2 inftm.0 0 ˙ = 0 W
3 inftm.x · ˙ = W
4 inftm.l < ˙ = < W
5 eleq1 x = X x B X B
6 eleq1 y = Y y B Y B
7 5 6 bi2anan9 x = X y = Y x B y B X B Y B
8 simpl x = X y = Y x = X
9 8 breq2d x = X y = Y 0 ˙ < ˙ x 0 ˙ < ˙ X
10 8 oveq2d x = X y = Y n · ˙ x = n · ˙ X
11 simpr x = X y = Y y = Y
12 10 11 breq12d x = X y = Y n · ˙ x < ˙ y n · ˙ X < ˙ Y
13 12 ralbidv x = X y = Y n n · ˙ x < ˙ y n n · ˙ X < ˙ Y
14 9 13 anbi12d x = X y = Y 0 ˙ < ˙ x n n · ˙ x < ˙ y 0 ˙ < ˙ X n n · ˙ X < ˙ Y
15 7 14 anbi12d x = X y = Y x B y B 0 ˙ < ˙ x n n · ˙ x < ˙ y X B Y B 0 ˙ < ˙ X n n · ˙ X < ˙ Y
16 eqid x y | x B y B 0 ˙ < ˙ x n n · ˙ x < ˙ y = x y | x B y B 0 ˙ < ˙ x n n · ˙ x < ˙ y
17 15 16 brabga X B Y B X x y | x B y B 0 ˙ < ˙ x n n · ˙ x < ˙ y Y X B Y B 0 ˙ < ˙ X n n · ˙ X < ˙ Y
18 17 3adant1 W V X B Y B X x y | x B y B 0 ˙ < ˙ x n n · ˙ x < ˙ y Y X B Y B 0 ˙ < ˙ X n n · ˙ X < ˙ Y
19 elex W V W V
20 19 3ad2ant1 W V X B Y B W V
21 fveq2 w = W Base w = Base W
22 21 1 syl6eqr w = W Base w = B
23 22 eleq2d w = W x Base w x B
24 22 eleq2d w = W y Base w y B
25 23 24 anbi12d w = W x Base w y Base w x B y B
26 fveq2 w = W 0 w = 0 W
27 26 2 syl6eqr w = W 0 w = 0 ˙
28 fveq2 w = W < w = < W
29 28 4 syl6eqr w = W < w = < ˙
30 eqidd w = W x = x
31 27 29 30 breq123d w = W 0 w < w x 0 ˙ < ˙ x
32 fveq2 w = W w = W
33 32 3 syl6eqr w = W w = · ˙
34 33 oveqd w = W n w x = n · ˙ x
35 eqidd w = W y = y
36 34 29 35 breq123d w = W n w x < w y n · ˙ x < ˙ y
37 36 ralbidv w = W n n w x < w y n n · ˙ x < ˙ y
38 31 37 anbi12d w = W 0 w < w x n n w x < w y 0 ˙ < ˙ x n n · ˙ x < ˙ y
39 25 38 anbi12d w = W x Base w y Base w 0 w < w x n n w x < w y x B y B 0 ˙ < ˙ x n n · ˙ x < ˙ y
40 39 opabbidv w = W x y | x Base w y Base w 0 w < w x n n w x < w y = x y | x B y B 0 ˙ < ˙ x n n · ˙ x < ˙ y
41 df-inftm = w V x y | x Base w y Base w 0 w < w x n n w x < w y
42 1 fvexi B V
43 42 42 xpex B × B V
44 opabssxp x y | x B y B 0 ˙ < ˙ x n n · ˙ x < ˙ y B × B
45 43 44 ssexi x y | x B y B 0 ˙ < ˙ x n n · ˙ x < ˙ y V
46 40 41 45 fvmpt W V W = x y | x B y B 0 ˙ < ˙ x n n · ˙ x < ˙ y
47 20 46 syl W V X B Y B W = x y | x B y B 0 ˙ < ˙ x n n · ˙ x < ˙ y
48 47 breqd W V X B Y B X W Y X x y | x B y B 0 ˙ < ˙ x n n · ˙ x < ˙ y Y
49 3simpc W V X B Y B X B Y B
50 49 biantrurd W V X B Y B 0 ˙ < ˙ X n n · ˙ X < ˙ Y X B Y B 0 ˙ < ˙ X n n · ˙ X < ˙ Y
51 18 48 50 3bitr4d W V X B Y B X W Y 0 ˙ < ˙ X n n · ˙ X < ˙ Y