This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lsmpropd

Description: If two structures have the same components (properties), they have the same subspace structure. (Contributed by Mario Carneiro, 29-Jun-2015) (Revised by AV, 25-Apr-2024)

Ref Expression
Hypotheses lsmpropd.b1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
lsmpropd.b2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
lsmpropd.p ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
lsmpropd.v1 ⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
lsmpropd.v2 ⊢ ( 𝜑 → 𝐿 ∈ 𝑊 )
Assertion lsmpropd ( 𝜑 → ( LSSum ‘ 𝐾 ) = ( LSSum ‘ 𝐿 ) )

Proof

Step Hyp Ref Expression
1 lsmpropd.b1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2 lsmpropd.b2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
3 lsmpropd.p ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
4 lsmpropd.v1 ⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
5 lsmpropd.v2 ⊢ ( 𝜑 → 𝐿 ∈ 𝑊 )
6 simp11 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑢 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝑡 ∧ 𝑦 ∈ 𝑢 ) → 𝜑 )
7 simp12 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑢 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝑡 ∧ 𝑦 ∈ 𝑢 ) → 𝑡 ∈ 𝒫 𝐵 )
8 7 elpwid ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑢 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝑡 ∧ 𝑦 ∈ 𝑢 ) → 𝑡 ⊆ 𝐵 )
9 simp2 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑢 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝑡 ∧ 𝑦 ∈ 𝑢 ) → 𝑥 ∈ 𝑡 )
10 8 9 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑢 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝑡 ∧ 𝑦 ∈ 𝑢 ) → 𝑥 ∈ 𝐵 )
11 simp13 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑢 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝑡 ∧ 𝑦 ∈ 𝑢 ) → 𝑢 ∈ 𝒫 𝐵 )
12 11 elpwid ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑢 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝑡 ∧ 𝑦 ∈ 𝑢 ) → 𝑢 ⊆ 𝐵 )
13 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑢 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝑡 ∧ 𝑦 ∈ 𝑢 ) → 𝑦 ∈ 𝑢 )
14 12 13 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑢 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝑡 ∧ 𝑦 ∈ 𝑢 ) → 𝑦 ∈ 𝐵 )
15 6 10 14 3 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑢 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝑡 ∧ 𝑦 ∈ 𝑢 ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
16 15 mpoeq3dva ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑢 ∈ 𝒫 𝐵 ) → ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ) = ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) ) )
17 16 rneqd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑢 ∈ 𝒫 𝐵 ) → ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ) = ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) ) )
18 17 mpoeq3dva ⊢ ( 𝜑 → ( 𝑡 ∈ 𝒫 𝐵 , 𝑢 ∈ 𝒫 𝐵 ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ) ) = ( 𝑡 ∈ 𝒫 𝐵 , 𝑢 ∈ 𝒫 𝐵 ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) ) ) )
19 1 pweqd ⊢ ( 𝜑 → 𝒫 𝐵 = 𝒫 ( Base ‘ 𝐾 ) )
20 mpoeq12 ⊢ ( ( 𝒫 𝐵 = 𝒫 ( Base ‘ 𝐾 ) ∧ 𝒫 𝐵 = 𝒫 ( Base ‘ 𝐾 ) ) → ( 𝑡 ∈ 𝒫 𝐵 , 𝑢 ∈ 𝒫 𝐵 ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ) ) = ( 𝑡 ∈ 𝒫 ( Base ‘ 𝐾 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝐾 ) ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ) ) )
21 19 19 20 syl2anc ⊢ ( 𝜑 → ( 𝑡 ∈ 𝒫 𝐵 , 𝑢 ∈ 𝒫 𝐵 ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ) ) = ( 𝑡 ∈ 𝒫 ( Base ‘ 𝐾 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝐾 ) ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ) ) )
22 2 pweqd ⊢ ( 𝜑 → 𝒫 𝐵 = 𝒫 ( Base ‘ 𝐿 ) )
23 mpoeq12 ⊢ ( ( 𝒫 𝐵 = 𝒫 ( Base ‘ 𝐿 ) ∧ 𝒫 𝐵 = 𝒫 ( Base ‘ 𝐿 ) ) → ( 𝑡 ∈ 𝒫 𝐵 , 𝑢 ∈ 𝒫 𝐵 ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) ) ) = ( 𝑡 ∈ 𝒫 ( Base ‘ 𝐿 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝐿 ) ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) ) ) )
24 22 22 23 syl2anc ⊢ ( 𝜑 → ( 𝑡 ∈ 𝒫 𝐵 , 𝑢 ∈ 𝒫 𝐵 ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) ) ) = ( 𝑡 ∈ 𝒫 ( Base ‘ 𝐿 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝐿 ) ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) ) ) )
25 18 21 24 3eqtr3d ⊢ ( 𝜑 → ( 𝑡 ∈ 𝒫 ( Base ‘ 𝐾 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝐾 ) ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ) ) = ( 𝑡 ∈ 𝒫 ( Base ‘ 𝐿 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝐿 ) ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) ) ) )
26 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
27 eqid ⊢ ( +g ‘ 𝐾 ) = ( +g ‘ 𝐾 )
28 eqid ⊢ ( LSSum ‘ 𝐾 ) = ( LSSum ‘ 𝐾 )
29 26 27 28 lsmfval ⊢ ( 𝐾 ∈ 𝑉 → ( LSSum ‘ 𝐾 ) = ( 𝑡 ∈ 𝒫 ( Base ‘ 𝐾 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝐾 ) ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ) ) )
30 4 29 syl ⊢ ( 𝜑 → ( LSSum ‘ 𝐾 ) = ( 𝑡 ∈ 𝒫 ( Base ‘ 𝐾 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝐾 ) ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ) ) )
31 eqid ⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
32 eqid ⊢ ( +g ‘ 𝐿 ) = ( +g ‘ 𝐿 )
33 eqid ⊢ ( LSSum ‘ 𝐿 ) = ( LSSum ‘ 𝐿 )
34 31 32 33 lsmfval ⊢ ( 𝐿 ∈ 𝑊 → ( LSSum ‘ 𝐿 ) = ( 𝑡 ∈ 𝒫 ( Base ‘ 𝐿 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝐿 ) ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) ) ) )
35 5 34 syl ⊢ ( 𝜑 → ( LSSum ‘ 𝐿 ) = ( 𝑡 ∈ 𝒫 ( Base ‘ 𝐿 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝐿 ) ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) ) ) )
36 25 30 35 3eqtr4d ⊢ ( 𝜑 → ( LSSum ‘ 𝐾 ) = ( LSSum ‘ 𝐿 ) )