Metamath Proof Explorer


Theorem djavalN

Description: Subspace join for DVecA partial vector space. (Contributed by NM, 6-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses djaval.h 𝐻 = ( LHyp ‘ 𝐾 )
djaval.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
djaval.i 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
djaval.n = ( ( ocA ‘ 𝐾 ) ‘ 𝑊 )
djaval.j 𝐽 = ( ( vA ‘ 𝐾 ) ‘ 𝑊 )
Assertion djavalN ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝑇𝑌𝑇 ) ) → ( 𝑋 𝐽 𝑌 ) = ( ‘ ( ( 𝑋 ) ∩ ( 𝑌 ) ) ) )

Proof

Step Hyp Ref Expression
1 djaval.h 𝐻 = ( LHyp ‘ 𝐾 )
2 djaval.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 djaval.i 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
4 djaval.n = ( ( ocA ‘ 𝐾 ) ‘ 𝑊 )
5 djaval.j 𝐽 = ( ( vA ‘ 𝐾 ) ‘ 𝑊 )
6 1 2 3 4 5 djafvalN ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝐽 = ( 𝑥 ∈ 𝒫 𝑇 , 𝑦 ∈ 𝒫 𝑇 ↦ ( ‘ ( ( 𝑥 ) ∩ ( 𝑦 ) ) ) ) )
7 6 adantr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝑇𝑌𝑇 ) ) → 𝐽 = ( 𝑥 ∈ 𝒫 𝑇 , 𝑦 ∈ 𝒫 𝑇 ↦ ( ‘ ( ( 𝑥 ) ∩ ( 𝑦 ) ) ) ) )
8 7 oveqd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝑇𝑌𝑇 ) ) → ( 𝑋 𝐽 𝑌 ) = ( 𝑋 ( 𝑥 ∈ 𝒫 𝑇 , 𝑦 ∈ 𝒫 𝑇 ↦ ( ‘ ( ( 𝑥 ) ∩ ( 𝑦 ) ) ) ) 𝑌 ) )
9 2 fvexi 𝑇 ∈ V
10 9 elpw2 ( 𝑋 ∈ 𝒫 𝑇𝑋𝑇 )
11 10 biimpri ( 𝑋𝑇𝑋 ∈ 𝒫 𝑇 )
12 11 ad2antrl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝑇𝑌𝑇 ) ) → 𝑋 ∈ 𝒫 𝑇 )
13 9 elpw2 ( 𝑌 ∈ 𝒫 𝑇𝑌𝑇 )
14 13 biimpri ( 𝑌𝑇𝑌 ∈ 𝒫 𝑇 )
15 14 ad2antll ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝑇𝑌𝑇 ) ) → 𝑌 ∈ 𝒫 𝑇 )
16 fvexd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝑇𝑌𝑇 ) ) → ( ‘ ( ( 𝑋 ) ∩ ( 𝑌 ) ) ) ∈ V )
17 fveq2 ( 𝑥 = 𝑋 → ( 𝑥 ) = ( 𝑋 ) )
18 17 ineq1d ( 𝑥 = 𝑋 → ( ( 𝑥 ) ∩ ( 𝑦 ) ) = ( ( 𝑋 ) ∩ ( 𝑦 ) ) )
19 18 fveq2d ( 𝑥 = 𝑋 → ( ‘ ( ( 𝑥 ) ∩ ( 𝑦 ) ) ) = ( ‘ ( ( 𝑋 ) ∩ ( 𝑦 ) ) ) )
20 fveq2 ( 𝑦 = 𝑌 → ( 𝑦 ) = ( 𝑌 ) )
21 20 ineq2d ( 𝑦 = 𝑌 → ( ( 𝑋 ) ∩ ( 𝑦 ) ) = ( ( 𝑋 ) ∩ ( 𝑌 ) ) )
22 21 fveq2d ( 𝑦 = 𝑌 → ( ‘ ( ( 𝑋 ) ∩ ( 𝑦 ) ) ) = ( ‘ ( ( 𝑋 ) ∩ ( 𝑌 ) ) ) )
23 eqid ( 𝑥 ∈ 𝒫 𝑇 , 𝑦 ∈ 𝒫 𝑇 ↦ ( ‘ ( ( 𝑥 ) ∩ ( 𝑦 ) ) ) ) = ( 𝑥 ∈ 𝒫 𝑇 , 𝑦 ∈ 𝒫 𝑇 ↦ ( ‘ ( ( 𝑥 ) ∩ ( 𝑦 ) ) ) )
24 19 22 23 ovmpog ( ( 𝑋 ∈ 𝒫 𝑇𝑌 ∈ 𝒫 𝑇 ∧ ( ‘ ( ( 𝑋 ) ∩ ( 𝑌 ) ) ) ∈ V ) → ( 𝑋 ( 𝑥 ∈ 𝒫 𝑇 , 𝑦 ∈ 𝒫 𝑇 ↦ ( ‘ ( ( 𝑥 ) ∩ ( 𝑦 ) ) ) ) 𝑌 ) = ( ‘ ( ( 𝑋 ) ∩ ( 𝑌 ) ) ) )
25 12 15 16 24 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝑇𝑌𝑇 ) ) → ( 𝑋 ( 𝑥 ∈ 𝒫 𝑇 , 𝑦 ∈ 𝒫 𝑇 ↦ ( ‘ ( ( 𝑥 ) ∩ ( 𝑦 ) ) ) ) 𝑌 ) = ( ‘ ( ( 𝑋 ) ∩ ( 𝑌 ) ) ) )
26 8 25 eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝑇𝑌𝑇 ) ) → ( 𝑋 𝐽 𝑌 ) = ( ‘ ( ( 𝑋 ) ∩ ( 𝑌 ) ) ) )