Metamath Proof Explorer


Theorem lcfrlem21

Description: Lemma for lcfr . (Contributed by NM, 11-Mar-2015)

Ref Expression
Hypotheses lcfrlem17.h 𝐻 = ( LHyp ‘ 𝐾 )
lcfrlem17.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
lcfrlem17.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
lcfrlem17.v 𝑉 = ( Base ‘ 𝑈 )
lcfrlem17.p + = ( +g𝑈 )
lcfrlem17.z 0 = ( 0g𝑈 )
lcfrlem17.n 𝑁 = ( LSpan ‘ 𝑈 )
lcfrlem17.a 𝐴 = ( LSAtoms ‘ 𝑈 )
lcfrlem17.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
lcfrlem17.x ( 𝜑𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
lcfrlem17.y ( 𝜑𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
lcfrlem17.ne ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
Assertion lcfrlem21 ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ‘ { ( 𝑋 + 𝑌 ) } ) ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 lcfrlem17.h 𝐻 = ( LHyp ‘ 𝐾 )
2 lcfrlem17.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 lcfrlem17.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 lcfrlem17.v 𝑉 = ( Base ‘ 𝑈 )
5 lcfrlem17.p + = ( +g𝑈 )
6 lcfrlem17.z 0 = ( 0g𝑈 )
7 lcfrlem17.n 𝑁 = ( LSpan ‘ 𝑈 )
8 lcfrlem17.a 𝐴 = ( LSAtoms ‘ 𝑈 )
9 lcfrlem17.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
10 lcfrlem17.x ( 𝜑𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
11 lcfrlem17.y ( 𝜑𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
12 lcfrlem17.ne ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
13 9 adantr ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( ‘ { ( 𝑋 + 𝑌 ) } ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
14 10 adantr ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( ‘ { ( 𝑋 + 𝑌 ) } ) ) → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
15 11 adantr ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( ‘ { ( 𝑋 + 𝑌 ) } ) ) → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
16 12 adantr ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( ‘ { ( 𝑋 + 𝑌 ) } ) ) → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
17 simpr ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( ‘ { ( 𝑋 + 𝑌 ) } ) ) → ¬ 𝑋 ∈ ( ‘ { ( 𝑋 + 𝑌 ) } ) )
18 1 2 3 4 5 6 7 8 13 14 15 16 17 lcfrlem20 ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( ‘ { ( 𝑋 + 𝑌 ) } ) ) → ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ‘ { ( 𝑋 + 𝑌 ) } ) ) ∈ 𝐴 )
19 1 3 9 dvhlmod ( 𝜑𝑈 ∈ LMod )
20 10 eldifad ( 𝜑𝑋𝑉 )
21 11 eldifad ( 𝜑𝑌𝑉 )
22 4 5 lmodcom ( ( 𝑈 ∈ LMod ∧ 𝑋𝑉𝑌𝑉 ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )
23 19 20 21 22 syl3anc ( 𝜑 → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )
24 23 sneqd ( 𝜑 → { ( 𝑋 + 𝑌 ) } = { ( 𝑌 + 𝑋 ) } )
25 24 fveq2d ( 𝜑 → ( ‘ { ( 𝑋 + 𝑌 ) } ) = ( ‘ { ( 𝑌 + 𝑋 ) } ) )
26 25 eleq2d ( 𝜑 → ( 𝑌 ∈ ( ‘ { ( 𝑋 + 𝑌 ) } ) ↔ 𝑌 ∈ ( ‘ { ( 𝑌 + 𝑋 ) } ) ) )
27 26 biimprd ( 𝜑 → ( 𝑌 ∈ ( ‘ { ( 𝑌 + 𝑋 ) } ) → 𝑌 ∈ ( ‘ { ( 𝑋 + 𝑌 ) } ) ) )
28 27 con3dimp ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( ‘ { ( 𝑋 + 𝑌 ) } ) ) → ¬ 𝑌 ∈ ( ‘ { ( 𝑌 + 𝑋 ) } ) )
29 prcom { 𝑋 , 𝑌 } = { 𝑌 , 𝑋 }
30 29 fveq2i ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( 𝑁 ‘ { 𝑌 , 𝑋 } )
31 30 a1i ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( 𝑁 ‘ { 𝑌 , 𝑋 } ) )
32 31 25 ineq12d ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ‘ { ( 𝑋 + 𝑌 ) } ) ) = ( ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∩ ( ‘ { ( 𝑌 + 𝑋 ) } ) ) )
33 32 adantr ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( ‘ { ( 𝑌 + 𝑋 ) } ) ) → ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ‘ { ( 𝑋 + 𝑌 ) } ) ) = ( ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∩ ( ‘ { ( 𝑌 + 𝑋 ) } ) ) )
34 9 adantr ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( ‘ { ( 𝑌 + 𝑋 ) } ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
35 11 adantr ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( ‘ { ( 𝑌 + 𝑋 ) } ) ) → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
36 10 adantr ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( ‘ { ( 𝑌 + 𝑋 ) } ) ) → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
37 12 necomd ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ≠ ( 𝑁 ‘ { 𝑋 } ) )
38 37 adantr ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( ‘ { ( 𝑌 + 𝑋 ) } ) ) → ( 𝑁 ‘ { 𝑌 } ) ≠ ( 𝑁 ‘ { 𝑋 } ) )
39 simpr ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( ‘ { ( 𝑌 + 𝑋 ) } ) ) → ¬ 𝑌 ∈ ( ‘ { ( 𝑌 + 𝑋 ) } ) )
40 1 2 3 4 5 6 7 8 34 35 36 38 39 lcfrlem20 ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( ‘ { ( 𝑌 + 𝑋 ) } ) ) → ( ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∩ ( ‘ { ( 𝑌 + 𝑋 ) } ) ) ∈ 𝐴 )
41 33 40 eqeltrd ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( ‘ { ( 𝑌 + 𝑋 ) } ) ) → ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ‘ { ( 𝑋 + 𝑌 ) } ) ) ∈ 𝐴 )
42 28 41 syldan ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( ‘ { ( 𝑋 + 𝑌 ) } ) ) → ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ‘ { ( 𝑋 + 𝑌 ) } ) ) ∈ 𝐴 )
43 1 2 3 4 5 6 7 8 9 10 11 12 lcfrlem19 ( 𝜑 → ( ¬ 𝑋 ∈ ( ‘ { ( 𝑋 + 𝑌 ) } ) ∨ ¬ 𝑌 ∈ ( ‘ { ( 𝑋 + 𝑌 ) } ) ) )
44 18 42 43 mpjaodan ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ‘ { ( 𝑋 + 𝑌 ) } ) ) ∈ 𝐴 )