Metamath Proof Explorer


Theorem lssvs0or

Description: If a scalar product belongs to a subspace, either the scalar component is zero or the vector component also belongs to the subspace. (Contributed by NM, 5-Apr-2015)

Ref Expression
Hypotheses lssvs0or.v V = Base W
lssvs0or.t · ˙ = W
lssvs0or.f F = Scalar W
lssvs0or.k K = Base F
lssvs0or.o 0 ˙ = 0 F
lssvs0or.s S = LSubSp W
lssvs0or.w φ W LVec
lssvs0or.u φ U S
lssvs0or.x φ X V
lssvs0or.a φ A K
Assertion lssvs0or φ A · ˙ X U A = 0 ˙ X U

Proof

Step Hyp Ref Expression
1 lssvs0or.v V = Base W
2 lssvs0or.t · ˙ = W
3 lssvs0or.f F = Scalar W
4 lssvs0or.k K = Base F
5 lssvs0or.o 0 ˙ = 0 F
6 lssvs0or.s S = LSubSp W
7 lssvs0or.w φ W LVec
8 lssvs0or.u φ U S
9 lssvs0or.x φ X V
10 lssvs0or.a φ A K
11 3 lvecdrng W LVec F DivRing
12 7 11 syl φ F DivRing
13 12 ad2antrr φ A · ˙ X U A 0 ˙ F DivRing
14 10 ad2antrr φ A · ˙ X U A 0 ˙ A K
15 simpr φ A · ˙ X U A 0 ˙ A 0 ˙
16 eqid F = F
17 eqid 1 F = 1 F
18 eqid inv r F = inv r F
19 4 5 16 17 18 drnginvrl F DivRing A K A 0 ˙ inv r F A F A = 1 F
20 13 14 15 19 syl3anc φ A · ˙ X U A 0 ˙ inv r F A F A = 1 F
21 20 oveq1d φ A · ˙ X U A 0 ˙ inv r F A F A · ˙ X = 1 F · ˙ X
22 lveclmod W LVec W LMod
23 7 22 syl φ W LMod
24 23 ad2antrr φ A · ˙ X U A 0 ˙ W LMod
25 4 5 18 drnginvrcl F DivRing A K A 0 ˙ inv r F A K
26 13 14 15 25 syl3anc φ A · ˙ X U A 0 ˙ inv r F A K
27 9 ad2antrr φ A · ˙ X U A 0 ˙ X V
28 1 3 2 4 16 lmodvsass W LMod inv r F A K A K X V inv r F A F A · ˙ X = inv r F A · ˙ A · ˙ X
29 24 26 14 27 28 syl13anc φ A · ˙ X U A 0 ˙ inv r F A F A · ˙ X = inv r F A · ˙ A · ˙ X
30 1 3 2 17 lmodvs1 W LMod X V 1 F · ˙ X = X
31 24 27 30 syl2anc φ A · ˙ X U A 0 ˙ 1 F · ˙ X = X
32 21 29 31 3eqtr3rd φ A · ˙ X U A 0 ˙ X = inv r F A · ˙ A · ˙ X
33 8 ad2antrr φ A · ˙ X U A 0 ˙ U S
34 simplr φ A · ˙ X U A 0 ˙ A · ˙ X U
35 3 2 4 6 lssvscl W LMod U S inv r F A K A · ˙ X U inv r F A · ˙ A · ˙ X U
36 24 33 26 34 35 syl22anc φ A · ˙ X U A 0 ˙ inv r F A · ˙ A · ˙ X U
37 32 36 eqeltrd φ A · ˙ X U A 0 ˙ X U
38 37 ex φ A · ˙ X U A 0 ˙ X U
39 38 necon1bd φ A · ˙ X U ¬ X U A = 0 ˙
40 39 orrd φ A · ˙ X U X U A = 0 ˙
41 40 orcomd φ A · ˙ X U A = 0 ˙ X U
42 oveq1 A = 0 ˙ A · ˙ X = 0 ˙ · ˙ X
43 42 adantl φ A = 0 ˙ A · ˙ X = 0 ˙ · ˙ X
44 eqid 0 W = 0 W
45 1 3 2 5 44 lmod0vs W LMod X V 0 ˙ · ˙ X = 0 W
46 23 9 45 syl2anc φ 0 ˙ · ˙ X = 0 W
47 44 6 lss0cl W LMod U S 0 W U
48 23 8 47 syl2anc φ 0 W U
49 46 48 eqeltrd φ 0 ˙ · ˙ X U
50 49 adantr φ A = 0 ˙ 0 ˙ · ˙ X U
51 43 50 eqeltrd φ A = 0 ˙ A · ˙ X U
52 23 adantr φ X U W LMod
53 8 adantr φ X U U S
54 10 adantr φ X U A K
55 simpr φ X U X U
56 3 2 4 6 lssvscl W LMod U S A K X U A · ˙ X U
57 52 53 54 55 56 syl22anc φ X U A · ˙ X U
58 51 57 jaodan φ A = 0 ˙ X U A · ˙ X U
59 41 58 impbida φ A · ˙ X U A = 0 ˙ X U