Metamath Proof Explorer


Theorem lsatcv0eq

Description: If the sum of two atoms cover the zero subspace, they are equal. ( atcv0eq analog.) (Contributed by NM, 10-Jan-2015)

Ref Expression
Hypotheses lsatcv0eq.o 0 = ( 0g𝑊 )
lsatcv0eq.p = ( LSSum ‘ 𝑊 )
lsatcv0eq.a 𝐴 = ( LSAtoms ‘ 𝑊 )
lsatcv0eq.c 𝐶 = ( ⋖L𝑊 )
lsatcv0eq.w ( 𝜑𝑊 ∈ LVec )
lsatcv0eq.q ( 𝜑𝑄𝐴 )
lsatcv0eq.r ( 𝜑𝑅𝐴 )
Assertion lsatcv0eq ( 𝜑 → ( { 0 } 𝐶 ( 𝑄 𝑅 ) ↔ 𝑄 = 𝑅 ) )

Proof

Step Hyp Ref Expression
1 lsatcv0eq.o 0 = ( 0g𝑊 )
2 lsatcv0eq.p = ( LSSum ‘ 𝑊 )
3 lsatcv0eq.a 𝐴 = ( LSAtoms ‘ 𝑊 )
4 lsatcv0eq.c 𝐶 = ( ⋖L𝑊 )
5 lsatcv0eq.w ( 𝜑𝑊 ∈ LVec )
6 lsatcv0eq.q ( 𝜑𝑄𝐴 )
7 lsatcv0eq.r ( 𝜑𝑅𝐴 )
8 1 3 5 6 7 lsatnem0 ( 𝜑 → ( 𝑄𝑅 ↔ ( 𝑄𝑅 ) = { 0 } ) )
9 eqid ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
10 lveclmod ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
11 5 10 syl ( 𝜑𝑊 ∈ LMod )
12 9 3 11 6 lsatlssel ( 𝜑𝑄 ∈ ( LSubSp ‘ 𝑊 ) )
13 9 2 1 3 4 5 12 7 lcvp ( 𝜑 → ( ( 𝑄𝑅 ) = { 0 } ↔ 𝑄 𝐶 ( 𝑄 𝑅 ) ) )
14 1 3 4 5 6 lsatcv0 ( 𝜑 → { 0 } 𝐶 𝑄 )
15 14 biantrurd ( 𝜑 → ( 𝑄 𝐶 ( 𝑄 𝑅 ) ↔ ( { 0 } 𝐶 𝑄𝑄 𝐶 ( 𝑄 𝑅 ) ) ) )
16 8 13 15 3bitrd ( 𝜑 → ( 𝑄𝑅 ↔ ( { 0 } 𝐶 𝑄𝑄 𝐶 ( 𝑄 𝑅 ) ) ) )
17 5 adantr ( ( 𝜑 ∧ ( { 0 } 𝐶 𝑄𝑄 𝐶 ( 𝑄 𝑅 ) ) ) → 𝑊 ∈ LVec )
18 1 9 lsssn0 ( 𝑊 ∈ LMod → { 0 } ∈ ( LSubSp ‘ 𝑊 ) )
19 11 18 syl ( 𝜑 → { 0 } ∈ ( LSubSp ‘ 𝑊 ) )
20 19 adantr ( ( 𝜑 ∧ ( { 0 } 𝐶 𝑄𝑄 𝐶 ( 𝑄 𝑅 ) ) ) → { 0 } ∈ ( LSubSp ‘ 𝑊 ) )
21 12 adantr ( ( 𝜑 ∧ ( { 0 } 𝐶 𝑄𝑄 𝐶 ( 𝑄 𝑅 ) ) ) → 𝑄 ∈ ( LSubSp ‘ 𝑊 ) )
22 9 3 11 7 lsatlssel ( 𝜑𝑅 ∈ ( LSubSp ‘ 𝑊 ) )
23 9 2 lsmcl ( ( 𝑊 ∈ LMod ∧ 𝑄 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑅 ∈ ( LSubSp ‘ 𝑊 ) ) → ( 𝑄 𝑅 ) ∈ ( LSubSp ‘ 𝑊 ) )
24 11 12 22 23 syl3anc ( 𝜑 → ( 𝑄 𝑅 ) ∈ ( LSubSp ‘ 𝑊 ) )
25 24 adantr ( ( 𝜑 ∧ ( { 0 } 𝐶 𝑄𝑄 𝐶 ( 𝑄 𝑅 ) ) ) → ( 𝑄 𝑅 ) ∈ ( LSubSp ‘ 𝑊 ) )
26 simprl ( ( 𝜑 ∧ ( { 0 } 𝐶 𝑄𝑄 𝐶 ( 𝑄 𝑅 ) ) ) → { 0 } 𝐶 𝑄 )
27 simprr ( ( 𝜑 ∧ ( { 0 } 𝐶 𝑄𝑄 𝐶 ( 𝑄 𝑅 ) ) ) → 𝑄 𝐶 ( 𝑄 𝑅 ) )
28 9 4 17 20 21 25 26 27 lcvntr ( ( 𝜑 ∧ ( { 0 } 𝐶 𝑄𝑄 𝐶 ( 𝑄 𝑅 ) ) ) → ¬ { 0 } 𝐶 ( 𝑄 𝑅 ) )
29 28 ex ( 𝜑 → ( ( { 0 } 𝐶 𝑄𝑄 𝐶 ( 𝑄 𝑅 ) ) → ¬ { 0 } 𝐶 ( 𝑄 𝑅 ) ) )
30 16 29 sylbid ( 𝜑 → ( 𝑄𝑅 → ¬ { 0 } 𝐶 ( 𝑄 𝑅 ) ) )
31 30 necon4ad ( 𝜑 → ( { 0 } 𝐶 ( 𝑄 𝑅 ) → 𝑄 = 𝑅 ) )
32 9 lsssssubg ( 𝑊 ∈ LMod → ( LSubSp ‘ 𝑊 ) ⊆ ( SubGrp ‘ 𝑊 ) )
33 11 32 syl ( 𝜑 → ( LSubSp ‘ 𝑊 ) ⊆ ( SubGrp ‘ 𝑊 ) )
34 33 12 sseldd ( 𝜑𝑄 ∈ ( SubGrp ‘ 𝑊 ) )
35 2 lsmidm ( 𝑄 ∈ ( SubGrp ‘ 𝑊 ) → ( 𝑄 𝑄 ) = 𝑄 )
36 34 35 syl ( 𝜑 → ( 𝑄 𝑄 ) = 𝑄 )
37 14 36 breqtrrd ( 𝜑 → { 0 } 𝐶 ( 𝑄 𝑄 ) )
38 oveq2 ( 𝑄 = 𝑅 → ( 𝑄 𝑄 ) = ( 𝑄 𝑅 ) )
39 38 breq2d ( 𝑄 = 𝑅 → ( { 0 } 𝐶 ( 𝑄 𝑄 ) ↔ { 0 } 𝐶 ( 𝑄 𝑅 ) ) )
40 37 39 syl5ibcom ( 𝜑 → ( 𝑄 = 𝑅 → { 0 } 𝐶 ( 𝑄 𝑅 ) ) )
41 31 40 impbid ( 𝜑 → ( { 0 } 𝐶 ( 𝑄 𝑅 ) ↔ 𝑄 = 𝑅 ) )