Metamath Proof Explorer


Theorem lsatcv1

Description: Two atoms covering the zero subspace are equal. ( atcv1 analog.) (Contributed by NM, 10-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 lsatcv1.o 0 = ( 0g𝑊 )
2 lsatcv1.p = ( LSSum ‘ 𝑊 )
3 lsatcv1.s 𝑆 = ( LSubSp ‘ 𝑊 )
4 lsatcv1.a 𝐴 = ( LSAtoms ‘ 𝑊 )
5 lsatcv1.c 𝐶 = ( ⋖L𝑊 )
6 lsatcv1.w ( 𝜑𝑊 ∈ LVec )
7 lsatcv1.u ( 𝜑𝑈𝑆 )
8 lsatcv1.q ( 𝜑𝑄𝐴 )
9 lsatcv1.r ( 𝜑𝑅𝐴 )
10 lsatcv1.l ( 𝜑𝑈 𝐶 ( 𝑄 𝑅 ) )
11 breq1 ( 𝑈 = { 0 } → ( 𝑈 𝐶 ( 𝑄 𝑅 ) ↔ { 0 } 𝐶 ( 𝑄 𝑅 ) ) )
12 10 11 syl5ibcom ( 𝜑 → ( 𝑈 = { 0 } → { 0 } 𝐶 ( 𝑄 𝑅 ) ) )
13 1 2 4 5 6 8 9 lsatcv0eq ( 𝜑 → ( { 0 } 𝐶 ( 𝑄 𝑅 ) ↔ 𝑄 = 𝑅 ) )
14 12 13 sylibd ( 𝜑 → ( 𝑈 = { 0 } → 𝑄 = 𝑅 ) )
15 10 adantr ( ( 𝜑𝑄 = 𝑅 ) → 𝑈 𝐶 ( 𝑄 𝑅 ) )
16 6 adantr ( ( 𝜑𝑄 = 𝑅 ) → 𝑊 ∈ LVec )
17 7 adantr ( ( 𝜑𝑄 = 𝑅 ) → 𝑈𝑆 )
18 oveq1 ( 𝑄 = 𝑅 → ( 𝑄 𝑅 ) = ( 𝑅 𝑅 ) )
19 lveclmod ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
20 6 19 syl ( 𝜑𝑊 ∈ LMod )
21 3 4 20 9 lsatlssel ( 𝜑𝑅𝑆 )
22 3 lsssubg ( ( 𝑊 ∈ LMod ∧ 𝑅𝑆 ) → 𝑅 ∈ ( SubGrp ‘ 𝑊 ) )
23 20 21 22 syl2anc ( 𝜑𝑅 ∈ ( SubGrp ‘ 𝑊 ) )
24 2 lsmidm ( 𝑅 ∈ ( SubGrp ‘ 𝑊 ) → ( 𝑅 𝑅 ) = 𝑅 )
25 23 24 syl ( 𝜑 → ( 𝑅 𝑅 ) = 𝑅 )
26 18 25 sylan9eqr ( ( 𝜑𝑄 = 𝑅 ) → ( 𝑄 𝑅 ) = 𝑅 )
27 9 adantr ( ( 𝜑𝑄 = 𝑅 ) → 𝑅𝐴 )
28 26 27 eqeltrd ( ( 𝜑𝑄 = 𝑅 ) → ( 𝑄 𝑅 ) ∈ 𝐴 )
29 1 3 4 5 16 17 28 lsatcveq0 ( ( 𝜑𝑄 = 𝑅 ) → ( 𝑈 𝐶 ( 𝑄 𝑅 ) ↔ 𝑈 = { 0 } ) )
30 15 29 mpbid ( ( 𝜑𝑄 = 𝑅 ) → 𝑈 = { 0 } )
31 30 ex ( 𝜑 → ( 𝑄 = 𝑅𝑈 = { 0 } ) )
32 14 31 impbid ( 𝜑 → ( 𝑈 = { 0 } ↔ 𝑄 = 𝑅 ) )