lsatcv1

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

	Ref	Expression
Hypotheses	lsatcv1.o	⊢ 0 = ( 0_g ‘ 𝑊 )
	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 = ( 0_g ‘ 𝑊 )
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 } ↔ 𝑄 = 𝑅 ) )

Metamath Proof Explorer

Theorem lsatcv1

Proof