Metamath Proof Explorer

Theorem xpsring1d

Description: The multiplicative identity element of a binary product of rings. (Contributed by AV, 16-Mar-2025)

Ref Expression
Hypotheses xpsringd.y ⊢ 𝑌 = ( 𝑆 ×s 𝑅 )
xpsringd.s ⊢ ( 𝜑 → 𝑆 ∈ Ring )
xpsringd.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
Assertion xpsring1d ( 𝜑 → ( 1r ‘ 𝑌 ) = ⟨ ( 1r ‘ 𝑆 ) , ( 1r ‘ 𝑅 ) ⟩ )

Proof

Step Hyp Ref Expression
1 xpsringd.y ⊢ 𝑌 = ( 𝑆 ×s 𝑅 )
2 xpsringd.s ⊢ ( 𝜑 → 𝑆 ∈ Ring )
3 xpsringd.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
4 eqid ⊢ ( mulGrp ‘ 𝑌 ) = ( mulGrp ‘ 𝑌 )
5 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
6 4 5 mgpbas ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ ( mulGrp ‘ 𝑌 ) )
7 eqid ⊢ ( 1r ‘ 𝑌 ) = ( 1r ‘ 𝑌 )
8 4 7 ringidval ⊢ ( 1r ‘ 𝑌 ) = ( 0g ‘ ( mulGrp ‘ 𝑌 ) )
9 eqid ⊢ ( .r ‘ 𝑌 ) = ( .r ‘ 𝑌 )
10 4 9 mgpplusg ⊢ ( .r ‘ 𝑌 ) = ( +g ‘ ( mulGrp ‘ 𝑌 ) )
11 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
12 eqid ⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
13 11 12 ringidcl ⊢ ( 𝑆 ∈ Ring → ( 1r ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) )
14 2 13 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) )
15 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
16 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
17 15 16 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
18 3 17 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
19 14 18 opelxpd ⊢ ( 𝜑 → ⟨ ( 1r ‘ 𝑆 ) , ( 1r ‘ 𝑅 ) ⟩ ∈ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑅 ) ) )
20 1 11 15 2 3 xpsbas ⊢ ( 𝜑 → ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑅 ) ) = ( Base ‘ 𝑌 ) )
21 19 20 eleqtrd ⊢ ( 𝜑 → ⟨ ( 1r ‘ 𝑆 ) , ( 1r ‘ 𝑅 ) ⟩ ∈ ( Base ‘ 𝑌 ) )
22 20 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑅 ) ) ↔ 𝑥 ∈ ( Base ‘ 𝑌 ) ) )
23 elxp2 ⊢ ( 𝑥 ∈ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑅 ) ) ↔ ∃ 𝑎 ∈ ( Base ‘ 𝑆 ) ∃ 𝑏 ∈ ( Base ‘ 𝑅 ) 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ )
24 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑆 ∈ Ring )
25 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑅 ∈ Ring )
26 14 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ( 1r ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) )
27 18 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
28 simprl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑎 ∈ ( Base ‘ 𝑆 ) )
29 simprr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑏 ∈ ( Base ‘ 𝑅 ) )
30 eqid ⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
31 11 30 24 26 28 ringcld ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 1r ‘ 𝑆 ) ( .r ‘ 𝑆 ) 𝑎 ) ∈ ( Base ‘ 𝑆 ) )
32 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
33 15 32 25 27 29 ringcld ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( Base ‘ 𝑅 ) )
34 1 11 15 24 25 26 27 28 29 31 33 30 32 9 xpsmul ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ( ⟨ ( 1r ‘ 𝑆 ) , ( 1r ‘ 𝑅 ) ⟩ ( .r ‘ 𝑌 ) ⟨ 𝑎 , 𝑏 ⟩ ) = ⟨ ( ( 1r ‘ 𝑆 ) ( .r ‘ 𝑆 ) 𝑎 ) , ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑏 ) ⟩ )
35 simpl ⊢ ( ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) → 𝑎 ∈ ( Base ‘ 𝑆 ) )
36 11 30 12 ringlidm ⊢ ( ( 𝑆 ∈ Ring ∧ 𝑎 ∈ ( Base ‘ 𝑆 ) ) → ( ( 1r ‘ 𝑆 ) ( .r ‘ 𝑆 ) 𝑎 ) = 𝑎 )
37 2 35 36 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 1r ‘ 𝑆 ) ( .r ‘ 𝑆 ) 𝑎 ) = 𝑎 )
38 simpr ⊢ ( ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) → 𝑏 ∈ ( Base ‘ 𝑅 ) )
39 15 32 16 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑏 ) = 𝑏 )
40 3 38 39 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑏 ) = 𝑏 )
41 37 40 opeq12d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ⟨ ( ( 1r ‘ 𝑆 ) ( .r ‘ 𝑆 ) 𝑎 ) , ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑏 ) ⟩ = ⟨ 𝑎 , 𝑏 ⟩ )
42 34 41 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ( ⟨ ( 1r ‘ 𝑆 ) , ( 1r ‘ 𝑅 ) ⟩ ( .r ‘ 𝑌 ) ⟨ 𝑎 , 𝑏 ⟩ ) = ⟨ 𝑎 , 𝑏 ⟩ )
43 oveq2 ⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ⟨ ( 1r ‘ 𝑆 ) , ( 1r ‘ 𝑅 ) ⟩ ( .r ‘ 𝑌 ) 𝑥 ) = ( ⟨ ( 1r ‘ 𝑆 ) , ( 1r ‘ 𝑅 ) ⟩ ( .r ‘ 𝑌 ) ⟨ 𝑎 , 𝑏 ⟩ ) )
44 id ⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ )
45 43 44 eqeq12d ⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( ⟨ ( 1r ‘ 𝑆 ) , ( 1r ‘ 𝑅 ) ⟩ ( .r ‘ 𝑌 ) 𝑥 ) = 𝑥 ↔ ( ⟨ ( 1r ‘ 𝑆 ) , ( 1r ‘ 𝑅 ) ⟩ ( .r ‘ 𝑌 ) ⟨ 𝑎 , 𝑏 ⟩ ) = ⟨ 𝑎 , 𝑏 ⟩ ) )
46 42 45 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ⟨ ( 1r ‘ 𝑆 ) , ( 1r ‘ 𝑅 ) ⟩ ( .r ‘ 𝑌 ) 𝑥 ) = 𝑥 ) )
47 46 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ( Base ‘ 𝑆 ) ∃ 𝑏 ∈ ( Base ‘ 𝑅 ) 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ⟨ ( 1r ‘ 𝑆 ) , ( 1r ‘ 𝑅 ) ⟩ ( .r ‘ 𝑌 ) 𝑥 ) = 𝑥 ) )
48 23 47 biimtrid ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑅 ) ) → ( ⟨ ( 1r ‘ 𝑆 ) , ( 1r ‘ 𝑅 ) ⟩ ( .r ‘ 𝑌 ) 𝑥 ) = 𝑥 ) )
49 22 48 sylbird ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝑌 ) → ( ⟨ ( 1r ‘ 𝑆 ) , ( 1r ‘ 𝑅 ) ⟩ ( .r ‘ 𝑌 ) 𝑥 ) = 𝑥 ) )
50 49 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑌 ) ) → ( ⟨ ( 1r ‘ 𝑆 ) , ( 1r ‘ 𝑅 ) ⟩ ( .r ‘ 𝑌 ) 𝑥 ) = 𝑥 )
51 11 30 24 28 26 ringcld ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑎 ( .r ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) ∈ ( Base ‘ 𝑆 ) )
52 15 32 25 29 27 ringcld ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑏 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
53 1 11 15 24 25 28 29 26 27 51 52 30 32 9 xpsmul ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ( ⟨ 𝑎 , 𝑏 ⟩ ( .r ‘ 𝑌 ) ⟨ ( 1r ‘ 𝑆 ) , ( 1r ‘ 𝑅 ) ⟩ ) = ⟨ ( 𝑎 ( .r ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) , ( 𝑏 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ⟩ )
54 11 30 12 ringridm ⊢ ( ( 𝑆 ∈ Ring ∧ 𝑎 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑎 ( .r ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) = 𝑎 )
55 2 35 54 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑎 ( .r ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) = 𝑎 )
56 15 32 16 ringridm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑏 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 𝑏 )
57 3 38 56 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑏 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 𝑏 )
58 55 57 opeq12d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ⟨ ( 𝑎 ( .r ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) , ( 𝑏 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ⟩ = ⟨ 𝑎 , 𝑏 ⟩ )
59 53 58 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ( ⟨ 𝑎 , 𝑏 ⟩ ( .r ‘ 𝑌 ) ⟨ ( 1r ‘ 𝑆 ) , ( 1r ‘ 𝑅 ) ⟩ ) = ⟨ 𝑎 , 𝑏 ⟩ )
60 oveq1 ⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑥 ( .r ‘ 𝑌 ) ⟨ ( 1r ‘ 𝑆 ) , ( 1r ‘ 𝑅 ) ⟩ ) = ( ⟨ 𝑎 , 𝑏 ⟩ ( .r ‘ 𝑌 ) ⟨ ( 1r ‘ 𝑆 ) , ( 1r ‘ 𝑅 ) ⟩ ) )
61 60 44 eqeq12d ⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝑥 ( .r ‘ 𝑌 ) ⟨ ( 1r ‘ 𝑆 ) , ( 1r ‘ 𝑅 ) ⟩ ) = 𝑥 ↔ ( ⟨ 𝑎 , 𝑏 ⟩ ( .r ‘ 𝑌 ) ⟨ ( 1r ‘ 𝑆 ) , ( 1r ‘ 𝑅 ) ⟩ ) = ⟨ 𝑎 , 𝑏 ⟩ ) )
62 59 61 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑥 ( .r ‘ 𝑌 ) ⟨ ( 1r ‘ 𝑆 ) , ( 1r ‘ 𝑅 ) ⟩ ) = 𝑥 ) )
63 62 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ( Base ‘ 𝑆 ) ∃ 𝑏 ∈ ( Base ‘ 𝑅 ) 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑥 ( .r ‘ 𝑌 ) ⟨ ( 1r ‘ 𝑆 ) , ( 1r ‘ 𝑅 ) ⟩ ) = 𝑥 ) )
64 23 63 biimtrid ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑅 ) ) → ( 𝑥 ( .r ‘ 𝑌 ) ⟨ ( 1r ‘ 𝑆 ) , ( 1r ‘ 𝑅 ) ⟩ ) = 𝑥 ) )
65 22 64 sylbird ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝑌 ) → ( 𝑥 ( .r ‘ 𝑌 ) ⟨ ( 1r ‘ 𝑆 ) , ( 1r ‘ 𝑅 ) ⟩ ) = 𝑥 ) )
66 65 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑌 ) ) → ( 𝑥 ( .r ‘ 𝑌 ) ⟨ ( 1r ‘ 𝑆 ) , ( 1r ‘ 𝑅 ) ⟩ ) = 𝑥 )
67 6 8 10 21 50 66 ismgmid2 ⊢ ( 𝜑 → ⟨ ( 1r ‘ 𝑆 ) , ( 1r ‘ 𝑅 ) ⟩ = ( 1r ‘ 𝑌 ) )
68 67 eqcomd ⊢ ( 𝜑 → ( 1r ‘ 𝑌 ) = ⟨ ( 1r ‘ 𝑆 ) , ( 1r ‘ 𝑅 ) ⟩ )