Theorem dsmmval

Description: Value of the module direct sum. (Contributed by Stefan O'Rear, 7-Jan-2015)

	Ref	Expression
Hypothesis	dsmmval.b	⊢ 𝐵 = { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin }
Assertion	dsmmval	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑆 ⊕m 𝑅 ) = ( ( 𝑆 Xs 𝑅 ) ↾s 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		dsmmval.b	⊢ 𝐵 = { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin }
2		elex	⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V )
3		oveq12	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → ( 𝑠 Xs 𝑟 ) = ( 𝑆 Xs 𝑅 ) )
4		eqid	⊢ ( 𝑠 Xs 𝑟 ) = ( 𝑠 Xs 𝑟 )
5		vex	⊢ 𝑠 ∈ V
6	5	a1i	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → 𝑠 ∈ V )
7		vex	⊢ 𝑟 ∈ V
8	7	a1i	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → 𝑟 ∈ V )
9		eqid	⊢ ( Base ‘ ( 𝑠 Xs 𝑟 ) ) = ( Base ‘ ( 𝑠 Xs 𝑟 ) )
10		eqidd	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → dom 𝑟 = dom 𝑟 )
11	4 6 8 9 10	prdsbas	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( 𝑠 Xs 𝑟 ) ) = X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) )
12	3	fveq2d	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( 𝑠 Xs 𝑟 ) ) = ( Base ‘ ( 𝑆 Xs 𝑅 ) ) )
13	11 12	eqtr3d	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) = ( Base ‘ ( 𝑆 Xs 𝑅 ) ) )
14		simpr	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → 𝑟 = 𝑅 )
15	14	dmeqd	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → dom 𝑟 = dom 𝑅 )
16	14	fveq1d	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → ( 𝑟 ‘ 𝑥 ) = ( 𝑅 ‘ 𝑥 ) )
17	16	fveq2d	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → ( 0g ‘ ( 𝑟 ‘ 𝑥 ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) )
18	17	neeq2d	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → ( ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑟 ‘ 𝑥 ) ) ↔ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
19	15 18	rabeqbidv	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → { 𝑥 ∈ dom 𝑟 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑟 ‘ 𝑥 ) ) } = { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } )
20	19	eleq1d	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → ( { 𝑥 ∈ dom 𝑟 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑟 ‘ 𝑥 ) ) } ∈ Fin ↔ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin ) )
21	13 20	rabeqbidv	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → { 𝑓 ∈ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ∣ { 𝑥 ∈ dom 𝑟 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑟 ‘ 𝑥 ) ) } ∈ Fin } = { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin } )
22	21 1	eqtr4di	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → { 𝑓 ∈ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ∣ { 𝑥 ∈ dom 𝑟 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑟 ‘ 𝑥 ) ) } ∈ Fin } = 𝐵 )
23	3 22	oveq12d	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → ( ( 𝑠 Xs 𝑟 ) ↾s { 𝑓 ∈ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ∣ { 𝑥 ∈ dom 𝑟 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑟 ‘ 𝑥 ) ) } ∈ Fin } ) = ( ( 𝑆 Xs 𝑅 ) ↾s 𝐵 ) )
24		df-dsmm	⊢ ⊕m = ( 𝑠 ∈ V , 𝑟 ∈ V ↦ ( ( 𝑠 Xs 𝑟 ) ↾s { 𝑓 ∈ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ∣ { 𝑥 ∈ dom 𝑟 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑟 ‘ 𝑥 ) ) } ∈ Fin } ) )
25		ovex	⊢ ( ( 𝑆 Xs 𝑅 ) ↾s 𝐵 ) ∈ V
26	23 24 25	ovmpoa	⊢ ( ( 𝑆 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑆 ⊕m 𝑅 ) = ( ( 𝑆 Xs 𝑅 ) ↾s 𝐵 ) )
27		reldmdsmm	⊢ Rel dom ⊕m
28	27	ovprc1	⊢ ( ¬ 𝑆 ∈ V → ( 𝑆 ⊕m 𝑅 ) = ∅ )
29		ress0	⊢ ( ∅ ↾s 𝐵 ) = ∅
30	28 29	eqtr4di	⊢ ( ¬ 𝑆 ∈ V → ( 𝑆 ⊕m 𝑅 ) = ( ∅ ↾s 𝐵 ) )
31		reldmprds	⊢ Rel dom Xs
32	31	ovprc1	⊢ ( ¬ 𝑆 ∈ V → ( 𝑆 Xs 𝑅 ) = ∅ )
33	32	oveq1d	⊢ ( ¬ 𝑆 ∈ V → ( ( 𝑆 Xs 𝑅 ) ↾s 𝐵 ) = ( ∅ ↾s 𝐵 ) )
34	30 33	eqtr4d	⊢ ( ¬ 𝑆 ∈ V → ( 𝑆 ⊕m 𝑅 ) = ( ( 𝑆 Xs 𝑅 ) ↾s 𝐵 ) )
35	34	adantr	⊢ ( ( ¬ 𝑆 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑆 ⊕m 𝑅 ) = ( ( 𝑆 Xs 𝑅 ) ↾s 𝐵 ) )
36	26 35	pm2.61ian	⊢ ( 𝑅 ∈ V → ( 𝑆 ⊕m 𝑅 ) = ( ( 𝑆 Xs 𝑅 ) ↾s 𝐵 ) )
37	2 36	syl	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑆 ⊕m 𝑅 ) = ( ( 𝑆 Xs 𝑅 ) ↾s 𝐵 ) )