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 ‘ 𝐿 ) )