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 = ( 0_g ‘ 𝑊 )
	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 = ( 0_g ‘ 𝑊 )
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 } 𝐶 ( 𝑄 ⊕ 𝑅 ) ↔ 𝑄 = 𝑅 ) )

Metamath Proof Explorer

Theorem lsatcv0eq

Proof