Metamath Proof Explorer


Theorem lcfrlem39

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

Ref Expression
Hypotheses lcfrlem38.h 𝐻 = ( LHyp ‘ 𝐾 )
lcfrlem38.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
lcfrlem38.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
lcfrlem38.p + = ( +g𝑈 )
lcfrlem38.f 𝐹 = ( LFnl ‘ 𝑈 )
lcfrlem38.l 𝐿 = ( LKer ‘ 𝑈 )
lcfrlem38.d 𝐷 = ( LDual ‘ 𝑈 )
lcfrlem38.q 𝑄 = ( LSubSp ‘ 𝐷 )
lcfrlem38.c 𝐶 = { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ‘ ( ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) }
lcfrlem38.e 𝐸 = 𝑔𝐺 ( ‘ ( 𝐿𝑔 ) )
lcfrlem38.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
lcfrlem38.g ( 𝜑𝐺𝑄 )
lcfrlem38.gs ( 𝜑𝐺𝐶 )
lcfrlem38.xe ( 𝜑𝑋𝐸 )
lcfrlem38.ye ( 𝜑𝑌𝐸 )
lcfrlem38.z 0 = ( 0g𝑈 )
lcfrlem38.x ( 𝜑𝑋0 )
lcfrlem38.y ( 𝜑𝑌0 )
lcfrlem38.sp 𝑁 = ( LSpan ‘ 𝑈 )
lcfrlem38.ne ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
lcfrlem38.b 𝐵 = ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ‘ { ( 𝑋 + 𝑌 ) } ) )
lcfrlem38.i ( 𝜑𝐼𝐵 )
lcfrlem38.n ( 𝜑𝐼0 )
Assertion lcfrlem39 ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ 𝐸 )

Proof

Step Hyp Ref Expression
1 lcfrlem38.h 𝐻 = ( LHyp ‘ 𝐾 )
2 lcfrlem38.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 lcfrlem38.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 lcfrlem38.p + = ( +g𝑈 )
5 lcfrlem38.f 𝐹 = ( LFnl ‘ 𝑈 )
6 lcfrlem38.l 𝐿 = ( LKer ‘ 𝑈 )
7 lcfrlem38.d 𝐷 = ( LDual ‘ 𝑈 )
8 lcfrlem38.q 𝑄 = ( LSubSp ‘ 𝐷 )
9 lcfrlem38.c 𝐶 = { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ‘ ( ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) }
10 lcfrlem38.e 𝐸 = 𝑔𝐺 ( ‘ ( 𝐿𝑔 ) )
11 lcfrlem38.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
12 lcfrlem38.g ( 𝜑𝐺𝑄 )
13 lcfrlem38.gs ( 𝜑𝐺𝐶 )
14 lcfrlem38.xe ( 𝜑𝑋𝐸 )
15 lcfrlem38.ye ( 𝜑𝑌𝐸 )
16 lcfrlem38.z 0 = ( 0g𝑈 )
17 lcfrlem38.x ( 𝜑𝑋0 )
18 lcfrlem38.y ( 𝜑𝑌0 )
19 lcfrlem38.sp 𝑁 = ( LSpan ‘ 𝑈 )
20 lcfrlem38.ne ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
21 lcfrlem38.b 𝐵 = ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ‘ { ( 𝑋 + 𝑌 ) } ) )
22 lcfrlem38.i ( 𝜑𝐼𝐵 )
23 lcfrlem38.n ( 𝜑𝐼0 )
24 eqid ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
25 eqid ( ·𝑠𝑈 ) = ( ·𝑠𝑈 )
26 eqid ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
27 eqid ( Base ‘ ( Scalar ‘ 𝑈 ) ) = ( Base ‘ ( Scalar ‘ 𝑈 ) )
28 oveq1 ( 𝑗 = 𝑘 → ( 𝑗 ( ·𝑠𝑈 ) 𝑥 ) = ( 𝑘 ( ·𝑠𝑈 ) 𝑥 ) )
29 28 oveq2d ( 𝑗 = 𝑘 → ( 𝑤 + ( 𝑗 ( ·𝑠𝑈 ) 𝑥 ) ) = ( 𝑤 + ( 𝑘 ( ·𝑠𝑈 ) 𝑥 ) ) )
30 29 eqeq2d ( 𝑗 = 𝑘 → ( 𝑣 = ( 𝑤 + ( 𝑗 ( ·𝑠𝑈 ) 𝑥 ) ) ↔ 𝑣 = ( 𝑤 + ( 𝑘 ( ·𝑠𝑈 ) 𝑥 ) ) ) )
31 30 rexbidv ( 𝑗 = 𝑘 → ( ∃ 𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑗 ( ·𝑠𝑈 ) 𝑥 ) ) ↔ ∃ 𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 ( ·𝑠𝑈 ) 𝑥 ) ) ) )
32 31 cbvriotavw ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∃ 𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑗 ( ·𝑠𝑈 ) 𝑥 ) ) ) = ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∃ 𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 ( ·𝑠𝑈 ) 𝑥 ) ) )
33 32 mpteq2i ( 𝑣 ∈ ( Base ‘ 𝑈 ) ↦ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∃ 𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑗 ( ·𝑠𝑈 ) 𝑥 ) ) ) ) = ( 𝑣 ∈ ( Base ‘ 𝑈 ) ↦ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∃ 𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 ( ·𝑠𝑈 ) 𝑥 ) ) ) )
34 33 mpteq2i ( 𝑥 ∈ ( ( Base ‘ 𝑈 ) ∖ { 0 } ) ↦ ( 𝑣 ∈ ( Base ‘ 𝑈 ) ↦ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∃ 𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑗 ( ·𝑠𝑈 ) 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ( ( Base ‘ 𝑈 ) ∖ { 0 } ) ↦ ( 𝑣 ∈ ( Base ‘ 𝑈 ) ↦ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∃ 𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 ( ·𝑠𝑈 ) 𝑥 ) ) ) ) )
35 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 34 lcfrlem38 ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ 𝐸 )