Metamath Proof Explorer


Theorem nmoleub2lem3

Description: Lemma for nmoleub2a and similar theorems. (Contributed by Mario Carneiro, 19-Oct-2015) (Proof shortened by AV, 29-Sep-2021)

Ref Expression
Hypotheses nmoleub2.n N = S normOp T
nmoleub2.v V = Base S
nmoleub2.l L = norm S
nmoleub2.m M = norm T
nmoleub2.g G = Scalar S
nmoleub2.w K = Base G
nmoleub2.s φ S NrmMod CMod
nmoleub2.t φ T NrmMod CMod
nmoleub2.f φ F S LMHom T
nmoleub2.a φ A *
nmoleub2.r φ R +
nmoleub2a.5 φ K
nmoleub2lem3.p · ˙ = S
nmoleub2lem3.1 φ A
nmoleub2lem3.2 φ 0 A
nmoleub2lem3.3 φ B V
nmoleub2lem3.4 φ B 0 S
nmoleub2lem3.5 φ r · ˙ B V L r · ˙ B < R M F r · ˙ B R A
nmoleub2lem3.6 φ ¬ M F B A L B
Assertion nmoleub2lem3 ¬ φ

Proof

Step Hyp Ref Expression
1 nmoleub2.n N = S normOp T
2 nmoleub2.v V = Base S
3 nmoleub2.l L = norm S
4 nmoleub2.m M = norm T
5 nmoleub2.g G = Scalar S
6 nmoleub2.w K = Base G
7 nmoleub2.s φ S NrmMod CMod
8 nmoleub2.t φ T NrmMod CMod
9 nmoleub2.f φ F S LMHom T
10 nmoleub2.a φ A *
11 nmoleub2.r φ R +
12 nmoleub2a.5 φ K
13 nmoleub2lem3.p · ˙ = S
14 nmoleub2lem3.1 φ A
15 nmoleub2lem3.2 φ 0 A
16 nmoleub2lem3.3 φ B V
17 nmoleub2lem3.4 φ B 0 S
18 nmoleub2lem3.5 φ r · ˙ B V L r · ˙ B < R M F r · ˙ B R A
19 nmoleub2lem3.6 φ ¬ M F B A L B
20 simprl φ r A R M F B < r r < R L B A R M F B < r
21 qre r r
22 21 ad2antlr φ r A R M F B < r r < R L B r
23 11 rpred φ R
24 14 23 remulcld φ A R
25 8 elin1d φ T NrmMod
26 nlmngp T NrmMod T NrmGrp
27 25 26 syl φ T NrmGrp
28 eqid Base T = Base T
29 2 28 lmhmf F S LMHom T F : V Base T
30 9 29 syl φ F : V Base T
31 30 16 ffvelrnd φ F B Base T
32 28 4 nmcl T NrmGrp F B Base T M F B
33 27 31 32 syl2anc φ M F B
34 0red φ 0
35 7 elin1d φ S NrmMod
36 nlmngp S NrmMod S NrmGrp
37 35 36 syl φ S NrmGrp
38 2 3 nmcl S NrmGrp B V L B
39 37 16 38 syl2anc φ L B
40 14 39 remulcld φ A L B
41 2 3 nmge0 S NrmGrp B V 0 L B
42 37 16 41 syl2anc φ 0 L B
43 14 39 15 42 mulge0d φ 0 A L B
44 40 33 ltnled φ A L B < M F B ¬ M F B A L B
45 19 44 mpbird φ A L B < M F B
46 34 40 33 43 45 lelttrd φ 0 < M F B
47 33 46 elrpd φ M F B +
48 24 47 rerpdivcld φ A R M F B
49 48 ad2antrr φ r A R M F B < r r < R L B A R M F B
50 9 ad2antrr φ r A R M F B < r r < R L B F S LMHom T
51 12 sselda φ r r K
52 51 adantr φ r A R M F B < r r < R L B r K
53 16 ad2antrr φ r A R M F B < r r < R L B B V
54 eqid T = T
55 5 6 2 13 54 lmhmlin F S LMHom T r K B V F r · ˙ B = r T F B
56 50 52 53 55 syl3anc φ r A R M F B < r r < R L B F r · ˙ B = r T F B
57 56 fveq2d φ r A R M F B < r r < R L B M F r · ˙ B = M r T F B
58 25 ad2antrr φ r A R M F B < r r < R L B T NrmMod
59 eqid Scalar T = Scalar T
60 5 59 lmhmsca F S LMHom T Scalar T = G
61 50 60 syl φ r A R M F B < r r < R L B Scalar T = G
62 61 fveq2d φ r A R M F B < r r < R L B Base Scalar T = Base G
63 62 6 syl6eqr φ r A R M F B < r r < R L B Base Scalar T = K
64 52 63 eleqtrrd φ r A R M F B < r r < R L B r Base Scalar T
65 31 ad2antrr φ r A R M F B < r r < R L B F B Base T
66 eqid Base Scalar T = Base Scalar T
67 eqid norm Scalar T = norm Scalar T
68 28 4 54 59 66 67 nmvs T NrmMod r Base Scalar T F B Base T M r T F B = norm Scalar T r M F B
69 58 64 65 68 syl3anc φ r A R M F B < r r < R L B M r T F B = norm Scalar T r M F B
70 61 fveq2d φ r A R M F B < r r < R L B norm Scalar T = norm G
71 70 fveq1d φ r A R M F B < r r < R L B norm Scalar T r = norm G r
72 7 elin2d φ S CMod
73 72 ad2antrr φ r A R M F B < r r < R L B S CMod
74 5 6 clmabs S CMod r K r = norm G r
75 73 52 74 syl2anc φ r A R M F B < r r < R L B r = norm G r
76 0red φ r A R M F B < r r < R L B 0
77 11 rpge0d φ 0 R
78 14 23 15 77 mulge0d φ 0 A R
79 divge0 A R 0 A R M F B 0 < M F B 0 A R M F B
80 24 78 33 46 79 syl22anc φ 0 A R M F B
81 80 ad2antrr φ r A R M F B < r r < R L B 0 A R M F B
82 76 49 22 81 20 lelttrd φ r A R M F B < r r < R L B 0 < r
83 76 22 82 ltled φ r A R M F B < r r < R L B 0 r
84 22 83 absidd φ r A R M F B < r r < R L B r = r
85 75 84 eqtr3d φ r A R M F B < r r < R L B norm G r = r
86 71 85 eqtrd φ r A R M F B < r r < R L B norm Scalar T r = r
87 86 oveq1d φ r A R M F B < r r < R L B norm Scalar T r M F B = r M F B
88 57 69 87 3eqtrd φ r A R M F B < r r < R L B M F r · ˙ B = r M F B
89 88 oveq1d φ r A R M F B < r r < R L B M F r · ˙ B R = r M F B R
90 2 5 13 6 clmvscl S CMod r K B V r · ˙ B V
91 73 52 53 90 syl3anc φ r A R M F B < r r < R L B r · ˙ B V
92 35 ad2antrr φ r A R M F B < r r < R L B S NrmMod
93 eqid norm G = norm G
94 2 3 13 5 6 93 nmvs S NrmMod r K B V L r · ˙ B = norm G r L B
95 92 52 53 94 syl3anc φ r A R M F B < r r < R L B L r · ˙ B = norm G r L B
96 85 oveq1d φ r A R M F B < r r < R L B norm G r L B = r L B
97 95 96 eqtrd φ r A R M F B < r r < R L B L r · ˙ B = r L B
98 simprr φ r A R M F B < r r < R L B r < R L B
99 23 ad2antrr φ r A R M F B < r r < R L B R
100 eqid 0 S = 0 S
101 2 3 100 nmrpcl S NrmGrp B V B 0 S L B +
102 37 16 17 101 syl3anc φ L B +
103 102 rpregt0d φ L B 0 < L B
104 103 ad2antrr φ r A R M F B < r r < R L B L B 0 < L B
105 ltmuldiv r R L B 0 < L B r L B < R r < R L B
106 22 99 104 105 syl3anc φ r A R M F B < r r < R L B r L B < R r < R L B
107 98 106 mpbird φ r A R M F B < r r < R L B r L B < R
108 97 107 eqbrtrd φ r A R M F B < r r < R L B L r · ˙ B < R
109 18 ad2antrr φ r A R M F B < r r < R L B r · ˙ B V L r · ˙ B < R M F r · ˙ B R A
110 91 108 109 mp2d φ r A R M F B < r r < R L B M F r · ˙ B R A
111 89 110 eqbrtrrd φ r A R M F B < r r < R L B r M F B R A
112 33 ad2antrr φ r A R M F B < r r < R L B M F B
113 22 112 remulcld φ r A R M F B < r r < R L B r M F B
114 14 ad2antrr φ r A R M F B < r r < R L B A
115 11 ad2antrr φ r A R M F B < r r < R L B R +
116 113 114 115 ledivmul2d φ r A R M F B < r r < R L B r M F B R A r M F B A R
117 111 116 mpbid φ r A R M F B < r r < R L B r M F B A R
118 114 99 remulcld φ r A R M F B < r r < R L B A R
119 33 46 jca φ M F B 0 < M F B
120 119 ad2antrr φ r A R M F B < r r < R L B M F B 0 < M F B
121 lemuldiv r A R M F B 0 < M F B r M F B A R r A R M F B
122 22 118 120 121 syl3anc φ r A R M F B < r r < R L B r M F B A R r A R M F B
123 117 122 mpbid φ r A R M F B < r r < R L B r A R M F B
124 22 49 123 lensymd φ r A R M F B < r r < R L B ¬ A R M F B < r
125 20 124 pm2.21dd φ r A R M F B < r r < R L B M F B A L B
126 23 102 rerpdivcld φ R L B
127 14 recnd φ A
128 23 recnd φ R
129 39 recnd φ L B
130 mulass A R L B A R L B = A R L B
131 mul12 A R L B A R L B = R A L B
132 130 131 eqtrd A R L B A R L B = R A L B
133 127 128 129 132 syl3anc φ A R L B = R A L B
134 40 33 11 45 ltmul2dd φ R A L B < R M F B
135 133 134 eqbrtrd φ A R L B < R M F B
136 lt2mul2div A R L B 0 < L B R M F B 0 < M F B A R L B < R M F B A R M F B < R L B
137 24 103 23 119 136 syl22anc φ A R L B < R M F B A R M F B < R L B
138 135 137 mpbid φ A R M F B < R L B
139 qbtwnre A R M F B R L B A R M F B < R L B r A R M F B < r r < R L B
140 48 126 138 139 syl3anc φ r A R M F B < r r < R L B
141 125 140 r19.29a φ M F B A L B
142 141 19 pm2.65i ¬ φ